| 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
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