X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=a3bc1f39a02a6fb76213c7caf54de0bc798c3a3d;hb=d7eb6fad3e5afc0fc786c9a91ef64733120dfb43;hp=ea0353182fee037aa0e04a43908705cd81358be3;hpb=e68d72ccd8757ad6b8fbb69ec3462e1ef1161cf5;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index ea0353182..a3bc1f39a 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -447,11 +447,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2 ugraph
       else
-       raise (UnificationFailure (lazy "3"))
-         (* (sprintf
+       raise (UnificationFailure (lazy 
+          (sprintf
             "Can't unify %s with %s due to different constants"
             (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))) *)
+            (CicMetaSubst.ppterm subst t2)))) 
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 then
          fo_unif_subst_exp_named_subst 
@@ -594,11 +594,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        if t1 = t2 then
          subst, metasenv,ugraph
        else
-        raise (UnificationFailure (lazy "6.2"))
-          (* (sprintf
+        raise (UnificationFailure (lazy 
+           (sprintf
              "Can't unify %s with %s because they are not convertible"
              (CicMetaSubst.ppterm subst t1) 
-             (CicMetaSubst.ppterm subst t2))) *)
+             (CicMetaSubst.ppterm subst t2))))
    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
        let subst,metasenv,beta_expanded,ugraph1 =
          beta_expand_many 
@@ -697,12 +697,18 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
       CicPp.ppterm ty_t1
-    with _ -> "MALFORMED")
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppterm subst t2)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
       CicPp.ppterm ty_t2
-    with _ -> "MALFORMED")
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppcontext subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
     (CicMetaSubst.ppsubst subst) (Lazy.force msg))