Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-08 19:19:59 -0700 (Tue, 08 Jun 1999)
Revision: 2696
Log message:

      Added a comsistent way of coming up with a new name for a variable that needs to be renamed
      (for example, to avoid capturing during substitution).
      
      Please note: the renaming algorithm is likely be changed in the future,
      no part of the system should rely on the particular algorithm.
      

Changes  Path
+8 -0 metaprl/mllib/string_util.ml
+4 -0 metaprl/mllib/string_util.mli
+3 -10 metaprl/refiner/term_ds/term_base_ds.ml
+13 -22 metaprl/refiner/term_std/term_subst_std.ml
+2 -9 metaprl/theories/tactic/var.ml