Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 23:13:13 -0800 (Tue, 18 Jan 2005)
Revision: 6440
Log message:

      This changes how the rewriter handles free variables in the term paramerers
      (not redex) of a rewrite (or a rule). Bsically, the rwrriter is reasonably
      smart to allow those variables to be captured by the allowed contexts as
      appropriate and to disallow capture (by alpha-renaming, not by raising an
      exception) by the context that is not free in the parameter.
      
      P.S. This implements the algorithm outlined in
      https://lists.metaprl.org/mailman/private/metaprl-research/2005-January/000174.html
      

Changes  Path
+2 -2 metaprl/filter/base/filter_grammar.ml
+1 -1 metaprl/filter/base/filter_magic.ml
+1 -1 metaprl/filter/filter/filter_parse.ml
+4 -4 metaprl/filter/filter/filter_prog.ml
+1 -1 metaprl/filter/phobos/phobos_rewrite.ml
+10 -10 metaprl/refiner/refiner/refine.ml
+1 -1 metaprl/refiner/reflib/dform.ml
+1 -1 metaprl/refiner/reflib/term_dtable.ml
+2 -2 metaprl/refiner/reflib/term_match_table.ml
+10 -23 metaprl/refiner/refsig/rewrite_sig.ml
+10 -15 metaprl/refiner/rewrite/rewrite.ml
+131 -40 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -2 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+2 -0 metaprl/refiner/rewrite/rewrite_debug.ml
+96 -56 metaprl/refiner/rewrite/rewrite_match_redex.ml
+16 -32 metaprl/refiner/rewrite/rewrite_types.ml
+3 -3 metaprl/support/tactics/tactic_cache.ml
+1 -1 metaprl/tactics/proof/rewrite_boot.ml