Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-19 20:17:22 -0700 (Sun, 19 Oct 2003)
Revision: 5003
Log message:
This fixes a number of bugs in Term_std.
Now bug 76 is almost done - the only differences in proof status
bewteen Term_std and Term_ds are:
---
ds: Status: /core_type_check/fun_equal is a derived object with an incomplete proof (1 rule boxes, 69 primitive steps)
std: Status: /core_type_check/fun_equal is a derived object with a complete proof (1 rule boxes, 76 primitive steps)
ds: Status: /itt_cyclic_group/subg_isCyclic is a derived object with a complete proof (35 rule boxes, 18230 primitive steps)
std: Status: /itt_cyclic_group/subg_isCyclic is a derived object with a complete proof (35 rule boxes, 18298 primitive steps)
ds: Status: /itt_nat/int_div_rem is a derived object with a complete proof (51 rule boxes, 129005 primitive steps)
std: Status: /itt_nat/int_div_rem is a derived object with a complete proof (51 rule boxes, 128785 primitive steps)
ds: Status: /itt_nat/positive_rule1 is a derived object with a complete proof (38 rule boxes, 70360 primitive steps)
std: Status: /itt_nat/positive_rule1 is a derived object with an incomplete proof (38 rule boxes, 71208 primitive steps)
---
The /core_type_check/fun_equal one is a part of bug 95 (hard to figure out
until the blocking bug 94 is fixed).
Hopefully, Yegor would have some idea on what is going on in /itt_nat/positive_rule1.