Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-18 17:41:22 -0700 (Sat, 18 Jun 2005)
Revision: 7389
Log message:

      Unified two unification algorithms into one
      

Changes	Path
+1 -3	metaprl/refiner/reflib/Files
+7 -5	metaprl/refiner/reflib/jall.ml
+2 -1	metaprl/refiner/reflib/jordering.ml
+2 -0	metaprl/refiner/reflib/jordering.mli
+328 -2	metaprl/refiner/reflib/jtunify.ml
+49 -2	metaprl/refiner/reflib/jtunify.mli
+45 -0	metaprl/refiner/reflib/jtypes.ml
+3 -1	metaprl/refiner/reflib/jtypes.mli