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 |