Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 15:33:59 -0700 (Wed, 20 Jul 2005)
Revision: 7645
Log message:

      Until now Jprover used to replace all originally free variables with ground terms
      and than recover tham at the final stage.
      It also used to inject its own ground terms which are actually variables in certain sense.
      Aleksey complained about its interaction with nested sequents.
      All this is now gone, jprover injects no ground terms, all of them are now variables.
      
      The only side effect which you might not like is that I use Lm_symbol.new_number
      and during check-status this index goes beyond 900000 (may be even above a million),
      I don't know if it is ever exposed to a user. If this happens I can return to
      usage of local counters though it might complicate the code a bit.
      

Changes	Path
+95 -96	metaprl/refiner/reflib/jall.ml
+33 -13	metaprl/refiner/reflib/jordering.ml
+0 -11	metaprl/refiner/reflib/jtunify.ml
+1 -2	metaprl/refiner/reflib/jtypes.ml