Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-15 00:01:49 -0700 (Sun, 15 Jul 2001)
Revision: 3334
Log message:

      When a bound variable already exists in the goal, it should not be
      supplied in the rule argument to prevent it from being renamed.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_dprod.ml
+1 -1 metaprl/theories/itt/itt_dprod.mli
+1 -1 metaprl/theories/itt/itt_list.ml
+1 -1 metaprl/theories/itt/itt_list.mli
+8 -8 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_prod.ml
+1 -1 metaprl/theories/itt/itt_prod.mli
+1 -1 metaprl/theories/itt/itt_record_label0.ml
+2512 -3037 metaprl/theories/itt/itt_sort.prla