Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-25 01:13:08 -0800 (Tue, 25 Jan 2005)
Revision: 6503
Log message:

      The integer tactics had some code that made some weird assumtions about how
      rewriting works - the assumptions that just happen to be true with TERMS=ds,
      but not with TERMS=std. I've changed the code to something more "safe".
      

Changes	Path
+1 -0	metaprl/tactics/proof/tactic_boot_sig.ml
+1 -1	metaprl/theories/itt/itt_int_arith.ml
+1 -1	metaprl/theories/itt/itt_omega.ml
+1 -1	metaprl/theories/itt/itt_supinf.ml