X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=354ecd9e819424cccf20424c31f99604a0252212;hb=42e7448a9e2eb9c44a336f0f3e56c9249f46fcc6;hp=c204adf06457e91ff897b53130ace40e8f8e600c;hpb=fbf93abd486f756b826ac2565f0296ecb4941dc0;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c204adf06..354ecd9e8 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -523,8 +523,8 @@ let eval_command status cmd =
      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);
+         if not(CicPp.check name ty) then
+           MatitaLog.warn ("Bad name: " ^ name);
          assert (metasenv = metasenv');
          let goalno =
           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in