Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 18:06:23 -0800 (Tue, 09 Mar 2004)
Revision: 5444
Log message:

      Bug 165: Added support for alpha-renaming/alpha-conversion when matching
      against redeces with two or more occurrences of the same sequent context.
      
      The support is a bit incomplete (a match might fail when the term does
      match - see the XXX BUG comment in rewrite_match_redex.ml), but I am hoping
      that it would not occur in real life scenarious.
      

Changes	Path
+62 -19	metaprl/refiner/rewrite/rewrite_match_redex.ml
+2 -2	metaprl/refiner/term_gen/term_meta_gen.ml
+1 -0	metaprl/refiner/term_std/term_subst_std.ml