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