Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-10-28 16:14:59 -0800 (Tue, 28 Oct 2003)
Revision: 5045
Log message:

      Two debug variables debug_graph_arith1 and debug_graph_arith2 added.
      When first of them set to true, /itt_nat/positive_rule1/1/2/3 become incomplete for Term_ds in the same way as for Term_std with same unproved inequality 0+m>=(1+m)+-1+y.
      The only thing that happens when you set debug_graph_arith1 to true is several calls to TermMan.nth_hyp. Any comments?
      

Changes	Path
+54 -1	metaprl/refiner/reflib/arith.ml