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

      Extraction finally works!!!!!!!!!!
      

Changes  Path
+6 -7 metaprl/editor/ml/Makefile
+1 -0 metaprl/filter/base/filter_type.ml
+7 -7 metaprl/filter/base/filter_util.ml
+29 -7 metaprl/filter/filter/filter_parse.ml
+17 -5 metaprl/filter/filter/term_grammar.ml
+1 -1 metaprl/mk/defaults
+173 -60 metaprl/refiner/refiner/refine.ml
+13 -1 metaprl/refiner/refsig/refine_sig.ml
+2 -2 metaprl/refiner/refsig/rewrite_sig.ml
+1 -0 metaprl/refiner/refsig/term_meta_sig.ml
+1 -1 metaprl/refiner/rewrite/rewrite.ml
+38 -31 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+5 -0 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+1 -0 metaprl/support/shell/shell_state.ml
+2 -0 metaprl/theories/itt/itt_test.ml