Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 15:02:44 -0700 (Wed, 20 Aug 2003)
Revision: 4858
Log message:

      Better error message from unify_mm.
      

Changes	Path
+1 -1	metaprl/filter/base/filter_summary.ml
+1 -1	metaprl/refiner/refiner/refine_error.ml
+4 -1	metaprl/refiner/reflib/refine_exn.ml
+14 -11	metaprl/refiner/reflib/unify_mm.ml
+1 -1	metaprl/refiner/refsig/refine_error_sig.ml
+1 -1	metaprl/refiner/term_ds/term_subst_ds.ml
+1 -1	metaprl/refiner/term_std/term_subst_std.ml