From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Feb 2004 11:23:05 +0000 (+0000)
Subject: A type checking error report now prints also the metasenv.
X-Git-Tag: V_0_3_0~28
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdb9c1c0efcf68e15f0d7e63f5d92dc87d2b3ac9;p=helm.git

A type checking error report now prints also the metasenv.
---

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