Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 02:54:06 -0700 (Thu, 31 Jul 2003)
Revision: 4794
Log message:

      Sequent.maybe_new_var should avoid all free variables, not just the ones
      declared in the goal sequent.
      

Changes	Path
+5 -10	metaprl-branches/bound_contexts2/filter/boot/sequent_boot.ml
+5 -1	metaprl-branches/bound_contexts2/filter/boot/tactic_boot_sig.mlz
+14 -15	metaprl-branches/bound_contexts2/refiner/reflib/unify_mm.ml
+8 -5	metaprl-branches/bound_contexts2/support/tactics/var.ml
+1 -0	metaprl-branches/bound_contexts2/support/tactics/var.mli
+4 -6	metaprl-branches/bound_contexts2/theories/itt/itt_derive.ml