Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 05:35:40 -0700 (Wed, 25 May 2005)
Revision: 7328
Log message:

      Updated the "sequentialization of rewrtites" hack so that when it creates
      "H >- t1 ~ t2" out of "t1 <--> t2" it would also add "H" to the context
      bindings lists of all the variables in t1 and t2.
      

Changes  Path
+18 -6 metaprl/refiner/refiner/refine.ml
+20 -19 metaprl/support/shell/shell_rule.ml
+16 -3 metaprl/tactics/proof/proof_boot.ml
+735 -1239 metaprl/theories/fol/fol_itt_and.prla
+2697 -3453 metaprl/theories/itt/itt_bool.prla
+3066 -2869 metaprl/theories/itt/itt_cyclic_group.prla
+5908 -5752 metaprl/theories/itt/itt_field2.prla
+1377 -1275 metaprl/theories/itt/itt_hoas_debruijn.prla
+2110 -1981 metaprl/theories/itt/itt_hoas_vector.prla
+13721 -13545 metaprl/theories/itt/itt_int_arith.prla
+6669 -6648 metaprl/theories/itt/itt_int_base.prla
+9368 -9289 metaprl/theories/itt/itt_int_ext.prla
+3524 -3321 metaprl/theories/itt/itt_list2.prla
+4825 -3758 metaprl/theories/itt/itt_poly.prla
+9251 -8696 metaprl/theories/itt/itt_rat.prla
+9584 -10497 metaprl/theories/itt/itt_record.prla
+795 -453 metaprl/theories/itt/itt_record0.prla
+3638 -9067 metaprl/theories/itt/itt_record_exm.prla
+5650 -5961 metaprl/theories/itt/itt_record_renaming.prla
+6483 -5924 metaprl/theories/itt/itt_reflection.prla
+405 -380 metaprl/theories/itt/itt_rfun.prla
+1 -1 metaprl/theories/itt/itt_struct2.ml
+2534 -2490 metaprl/theories/itt/itt_synt_bterm.prla
+408 -382 metaprl/theories/itt/itt_synt_operator.prla
+3430 -3281 metaprl/theories/itt/itt_synt_subst.prla