Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-18 18:23:51 -0800 (Tue, 18 Mar 2003)
Revision: 4183
Log message:

      - The rewriter now correctly makes sure that the SO var args have
      to be distinct for it to be a potential "poattern" source (and not
      just an instance). This fixed BUGS 4.11 and allows eliminating the
      "HACK" terms in itt_*isect
      
      - free_vars_terms now returns StringSet.t, not string list
      

Changes  Path
+3 -16 metaprl/BUGS
+1 -1 metaprl/refiner/refiner/refine.ml
+1 -4 metaprl/refiner/refsig/term_subst_sig.ml
+1 -1 metaprl/refiner/rewrite/rewrite.ml
+1 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+9 -4 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+2 -4 metaprl/refiner/term_ds/term_subst_ds.ml
+2 -2 metaprl/refiner/term_std/term_subst_std.ml
+5 -5 metaprl/theories/itt/itt_bisect.ml
+5 -5 metaprl/theories/itt/itt_bisect.prla
+8 -8 metaprl/theories/itt/itt_disect.ml
+7 -7 metaprl/theories/itt/itt_disect.prla
+5 -6 metaprl/theories/itt/itt_isect.ml
+3 -3 metaprl/theories/itt/itt_isect.prla
+1 -1 metaprl/theories/tptp/tptp_prove.ml