X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9a87bc51bba07e6493a4666ae494a0fdce006a45;hb=af364f229a858464cc557e60e314b6ffb20b6625;hp=a2a98bd0d8213739796d81de2492cb1446b4242d;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index a2a98bd0d..9a87bc51b 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -46,6 +46,17 @@ let foo () =
          lazy
           (sprintf
            "Kernel Type checking error: 
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+             (CicMetaSubst.ppterm subst term)
+             (CicMetaSubst.ppterm [] term)
+             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppmetasenv subst metasenv) 
+             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+        raise (AssertFailure msg)
+    | CicTypeChecker.AssertFailure msg ->
+        let msg = lazy
+         (sprintf
+           "Kernel Type checking assertion failure: 
 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
              (CicMetaSubst.ppterm subst term)
              (CicMetaSubst.ppterm [] term)
@@ -574,7 +585,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           ) (subst'',metasenv'',ugraph2) pl1 pl2 
         with
          Invalid_argument _ ->
-          raise (UnificationFailure (lazy "6")))
+          raise (UnificationFailure (lazy "6.1")))
            (* (sprintf
               "Error trying to unify %s with %s: the number of branches is not the same." 
               (CicMetaSubst.ppterm subst t1) 
@@ -583,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"))
-          (* (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