From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 15 Jul 2005 11:18:23 +0000 (+0000)
Subject: Bad name should be an error and not just a warning.
X-Git-Tag: pre_notation~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b9dfee085d32e0c2f4e216130d92669a40aac733;p=helm.git

Bad name should be an error and not just a warning.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 94efb904f..c3a8be67d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -542,7 +542,7 @@ let eval_command opts status cmd =
      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
          if not(CicPp.check name ty) then
-           MatitaLog.warn ("Bad name: " ^ name);
+           MatitaLog.error ("Bad name: " ^ name);
          if opts.do_heavy_checks then
            begin
              let dbd = MatitaDb.instance () in