From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 18:48:22 +0000 (+0000)
Subject: AssertFailure from the type-checker now becomes an AssertFailure for the
X-Git-Tag: V_0_7_2_3~111
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e68d72ccd8757ad6b8fbb69ec3462e1ef1161cf5;p=helm.git

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 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)