From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 10:49:49 +0000 (+0000)
Subject: More informative error message.
X-Git-Tag: PRE_INDEX_1~42
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=badc43296cdc81e4376abe72071941317effe8b3;p=helm.git

More informative error message.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index ae933d2d0..6ca720830 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -343,8 +343,9 @@ let eval_command status cmd =
         CicUnification.fo_unif metasenv [] body_type ty ugraph
       in
       if metasenv <> [] then
-        command_error
-          "metasenv not empty while giving a definition with body";
+        command_error (
+          "metasenv not empty while giving a definition with body: " ^
+          CicMetaSubst.ppmetasenv metasenv []) ;
       let body = CicMetaSubst.apply_subst subst body in
       let ty = CicMetaSubst.apply_subst subst ty in
       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in