Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-03 22:47:44 -0700 (Wed, 03 May 2000)
Revision: 2952
Log message:
I started working on removing old (and buggy!) unification and speeding up
the new "MM" unification.
Note that all these changes are on the unify_mm branch, not the trunk. It means
that "cvs update" would not give you this changes unless you run it with "-r unify_mm"
option. This should allow people to continue working on the rest of the MetaPRL without
being affected by these changes.
This code would not compile until I finish doing tons of trivial changes in ITT typeinf
updates. (I just wish typeinf would already be implemented using resource annotations!)
Also, the TPTP code expects unification to raise RefineError exceptions,
but unification currently raises other kinds of exceptions. Hopefully, V.N.
will be able to fix this.
V.N. - can you double-check my changes? Thanks!