Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-12-09 12:44:49 -0800 (Thu, 09 Dec 1999)
Revision: 2868
Log message:

      The unifiable and unify_mm functions are inserted into TermSubst module
      

Changes	Path
+7 -0	metaprl/refiner/refsig/term_subst_sig.ml
+20 -0	metaprl/refiner/term_ds/term_subst_ds.ml
+7 -0	metaprl/refiner/term_std/term_subst_std.ml