X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=c5b2fb98774702ee955193f6872a191240cea8a8;hb=f263e4ec717d5ec2e7f9c057855f8223f81baae8;hp=b20755d870bb4a87def160f7f57d05e9ee7c12e4;hpb=fddf15f1e9d253316bdcb854c2ff7ec64144bde8;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b20755d87..c5b2fb987 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -410,7 +410,7 @@ let disambiguate_obj status obj =
     | TacticAst.Record (_,name,_,_) ->
        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
     | TacticAst.Inductive _ -> assert false
-    | _ -> None in
+    | TacticAst.Theorem _ -> None in
   let (aliases, metasenv, cic, _) =
     match
       MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
@@ -459,7 +459,11 @@ let eval_command status cmd =
   | TacticAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
-          MatitaMisc.strip_trailing_slash value
+          let v = MatitaMisc.strip_trailing_slash value in
+          try
+            ignore (String.index v ' ');
+            command_error "baseuri can't contain spaces"
+          with Not_found -> v
         else
           value
       in
@@ -518,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.warn ("Bad name: " ^ name);
          assert (metasenv = metasenv');
          let goalno =
           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in