AssertFailure from the type-checker now becomes an AssertFailure for the

unifier.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 7c0d0e387c8c1c278f4fceb6baa168f022d39439..ea0353182fee037aa0e04a43908705cd81358be3 100644 (file)
--- 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)