]> matita.cs.unibo.it Git - helm.git/commitdiff
More informative error message.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 8 Jun 2005 10:49:49 +0000 (10:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 8 Jun 2005 10:49:49 +0000 (10:49 +0000)
helm/matita/matitaEngine.ml

index ae933d2d0022a1f08d7dca832f633a8024840ebe..6ca72083008975c8365198a06225325cdc0d8807 100644 (file)
@@ -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