Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-11-14 12:56:11 -0800 (Sun, 14 Nov 1999)
Revision: 2849
Log message:

      The unify function is added into term_unif_ds. It unifies 2 terms and returnes a
      substitution.:
      

Changes	Path
+214 -20	metaprl/refiner/term_ds/term_unif_ds.ml
Added	metaprl/refiner/term_ds/term_unif_ds.mli
Properties	metaprl/refiner/term_ds/term_unif_ds.mli