Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-07 19:28:04 -0800 (Sat, 07 Feb 2004)
Revision: 5349
Log message:

      Were too careless in applying normalizeC
      (in order to normalize candidate inequalities for arithT) so it was applied to
      some terms it shouldn't have been to, and that injected some needless wf-subgoals.
      

Changes	Path
+6 -1	metaprl/theories/itt/itt_int_arith.ml