match obj with
Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
- if not(CicPp.check name ty) then
+ if not(CicPp.check name ty) then
MatitaLog.warn ("Bad name: " ^ name);
assert (metasenv = metasenv');
let goalno =