Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-21 13:16:08 -0700 (Fri, 21 May 2004)
Revision: 5800
Log message:

      Made a benchmarking:
      arithT(+normalizeC)  vs  arithT+itt_mpoly2.standardizeT
      on itt_int_arith/test* arithT+normalizeC is 12 times faster.
      Partly because of lot's of wf-subgoals.
      (There was an impression that a reflection based normalization
      is not supposed to make a lot of wf-subgoals.)
      Partly because of inefficient strategy of computation I guess.
      So I have to figure out what's going on. First, I'm going to strip out
      itt_mpoly2 computations into a separate resource (it's in reduce now)
      

Changes  Path
+148 -23 metaprl/theories/itt/itt_mpoly2.ml
+34 -0 metaprl/theories/itt/itt_mpoly2.mli
+10099 -6312 metaprl/theories/itt/itt_mpoly2.prla
Added metaprl/theories/itt/itt_mpoly2_bench.ml
Properties metaprl/theories/itt/itt_mpoly2_bench.ml
Added metaprl/theories/itt/itt_mpoly2_bench.mli
Properties metaprl/theories/itt/itt_mpoly2_bench.mli
Added metaprl/theories/itt/itt_mpoly2_bench.prla
Properties metaprl/theories/itt/itt_mpoly2_bench.prla