Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 19:25:05 -0700 (Fri, 21 May 2004)
Revision: 5802
Log message:

      Comented out the "crwhigher" refiner mechanism. The tactics module will now
      use the external mechanism for a higherC of a conditional rewrite.
      
      The above should make it harder (but not entirely impossible yet) to improperly
      lift a variable out of its scope by a conditional rewrite.
      

Changes  Path
+3 -2 metaprl/refiner/refiner/refine.ml
+2 -1 metaprl/refiner/refsig/refine_sig.ml
+1 -2 metaprl/refiner/refsig/rewrite_sig.ml
+4 -2 metaprl/tactics/proof/rewrite_boot.ml