X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=ea0353182fee037aa0e04a43908705cd81358be3;hb=062eb0af0b92e5f7f99f90fb453e9fd010b47e7a;hp=7c0d0e387c8c1c278f4fceb6baa168f022d39439;hpb=3813bdd5d0b4139a682b5faa50611791ac9278c2;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 7c0d0e387..ea0353182 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)