From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 7 Jul 2005 13:30:40 +0000 (+0000)
Subject: Raising an error on a bad theorem name.
X-Git-Tag: V_0_7_1~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fbf93abd486f756b826ac2565f0296ecb4941dc0;p=helm.git

Raising an error on a bad theorem name.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index ebcf0538a..c204adf06 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -522,6 +522,9 @@ let eval_command status cmd =
      let metasenv = MatitaMisc.get_proof_metasenv status in
      match obj with
         Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+         let name = UriManager.name_of_uri uri in
+	 if not(CicPp.check name ty) then
+           MatitaLog.error ("Bad name: "^name);
          assert (metasenv = metasenv');
          let goalno =
           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in