Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-15 16:31:35 -0800 (Tue, 15 Feb 2000)
Revision: 2883
Log message:

      Enabled the "strict" rewriter mode.
      
      In "strict" mode, <<lambda{x.'t}>> will only match terms where "t" does not contain
      free occurences of "x" while <<lambda{x.'t['x]}>> will match any lambda expression.
      In "relaxed" mode both redices will match any lambda expression.
      
      This is done
      1) To force rule authors to completely specify the binding structure
      2) To allow rule authors to specify free variables restrictions easier
      
      refiner/refiner/refine.ml, filter/boot/rewrite_boot.ml and theories/tactic/tactic_cache.ml
      use the strict mode.
      
      filter/base/filter_prog.ml uses relaxed mode for d.f. and compiles ml rewrites
      using the strict mode
      
      refiner/reflib/dform.ml, refiner/reflib/term_dtable.ml and refiner/reflib/term_match_table.ml
      use the relaxed mode.
      
      Please let me know if this change breaks something.
      

Changes  Path
+0 -7 metaprl/BUGS
+4 -2 metaprl/filter/base/filter_prog.ml
+1 -1 metaprl/filter/boot/rewrite_boot.ml
+6 -6 metaprl/refiner/refiner/refine.ml
+1 -1 metaprl/refiner/reflib/dform.ml
+1 -1 metaprl/refiner/reflib/term_dtable.ml
+1 -1 metaprl/refiner/reflib/term_match_table.ml
+14 -4 metaprl/refiner/refsig/rewrite_sig.ml
+6 -6 metaprl/refiner/rewrite/rewrite.ml
+10 -6 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -0 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+2 -1 metaprl/refiner/rewrite/rewrite_compile_redex_sig.mlz
+2 -2 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -0 metaprl/refiner/rewrite/rewrite_types.ml
+3 -3 metaprl/theories/tactic/tactic_cache.ml