Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-10 23:45:58 -0800 (Wed, 10 Mar 2004)
Revision: 5448
Log message:

      - Bug 159: allow context arguments in rewrites (but not in ML rewrites).
      - Other minor updates in filter_parse and filter_prog code.
      

Changes  Path
+4 -11 metaprl/filter/filter/filter_parse.ml
+19 -16 metaprl/filter/filter/filter_prog.ml
+5 -0 metaprl/filter/filter/term_grammar.ml
+12 -9 metaprl/refiner/refiner/refine.ml
+1 -0 metaprl/refiner/reflib/mp_resource.ml
+1 -0 metaprl/refiner/reflib/mp_resource.mli
+3 -1 metaprl/refiner/refsig/refine_sig.ml
+9 -9 metaprl/tactics/proof/rewrite_boot.ml
+1 -1 metaprl/tactics/proof/tactic_boot_sig.ml