Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-11-28 13:10:30 -0800 (Sun, 28 Nov 1999)
Revision: 2863
Log message:

      The TermSubstMm functor provides n*log n unifiability test
      and unify function time=O(#variables^2)
      

Changes	Path
+2 -1	metaprl/refiner/term_ds/Files
+202 -66	metaprl/refiner/term_ds/term_unif_ds.ml
+195 -62	metaprl/refiner/term_ds/term_unif_ds.mli