A type checking error report now prints also the metasenv.

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

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