Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-17 19:51:47 -0800 (Mon, 17 Mar 2003)
Revision: 4179
Log message:

      Fixed some (hopefull all!) bugs where rewrite mechanism was looking (counting
      hyps, taking subterms out, passing to nth*addr, etc) at the goal, while rewrite
      was being applied to an assumption.
      

Changes  Path
+2 -4 metaprl/filter/boot/conversionals_boot.ml
+26 -40 metaprl/filter/boot/rewrite_boot.ml
+7 -3 metaprl/filter/boot/sequent_boot.ml
+2 -3 metaprl/filter/boot/tactic_boot.ml
+5 -11 metaprl/filter/boot/tactic_boot_sig.mlz
+14 -30 metaprl/filter/boot/tacticals_boot.ml
+2 -1 metaprl/refiner/refsig/term_man_sig.ml
+0 -1 metaprl/theories/tactic/top_conversionals.ml
+0 -1 metaprl/theories/tactic/top_conversionals.mli
+1 -2 metaprl/theories/tactic/top_tacticals.ml
+0 -1 metaprl/theories/tactic/top_tacticals.mli