Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-05-07 07:22:07 -0700 (Sun, 07 May 2000)
Revision: 2958
Log message:

      The RefineError exceptins are incorporated correctly in Term_unif_ds module
      

Changes	Path
+94 -47	metaprl-branches/unify_mm/refiner/term_ds/term_unif_ds.ml