From e68d72ccd8757ad6b8fbb69ec3462e1ef1161cf5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 18:48:22 +0000 Subject: [PATCH] AssertFailure from the type-checker now becomes an AssertFailure for the unifier. --- helm/ocaml/cic_unification/cicUnification.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) 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) -- 2.39.2