Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-05 00:10:12 -0700 (Fri, 05 Sep 2003)
Revision: 4935
Log message:

      - Changed the way mp_version.ml is hapdled to be a -pp hack on a static .ml file.
      This will likely break Win32 build! :-(
      
      - Added checks that make sure that the extract passed into Refiner really proves
      what it was supposed to prove. This requires moving a HACK that creates sequent
      representation of rewrites into the Refine module :-(
      

Changes  Path
+4 -4 metaprl/OMakefile
+10 -14 metaprl/editor/ml/OMakefile
Added metaprl/editor/ml/mp_version.ml
Properties metaprl/editor/ml/mp_version.ml
+3 -0 metaprl/filter/filter/prlcomp.ml
+35 -31 metaprl/refiner/refiner/refine.ml
+4 -0 metaprl/refiner/refsig/refine_sig.ml
+0 -12 metaprl/support/shell/shell_rewrite.ml