From cdb9c1c0efcf68e15f0d7e63f5d92dc87d2b3ac9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Feb 2004 11:23:05 +0000 Subject: [PATCH] A type checking error report now prints also the metasenv. --- helm/ocaml/cic_unification/cicUnification.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index bf035d74a..90eacc568 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -38,9 +38,10 @@ let type_of_aux' metasenv subst context term = | CicMetaSubst.MetaSubstFailure msg -> raise (AssertFailure ((sprintf - "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" + "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppcontext subst context) msg))) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv metasenv subst) msg))) (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a -- 2.39.2