Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 11:09:16 -0700 (Thu, 21 Jul 2005)
Revision: 7652
Log message:

      I started to work on rule-based prefix unification in jprover.
      The potential benefits:
      1.It's easier to adapt to other logics
      2.One of possible resolutions for contination problem
      
      Right now it's pretty naive and check-status is 50secs slower but
      s4_tests/mch3 which used to run for 120 secs runs for 80 secs now.
      I think the latter speed up is due to tail-recursive code of this new
      implementation.
      

Changes	Path
+159 -150	metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml