- Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+ | 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);
+ if opts.do_heavy_checks then
+ begin
+ let dbd = MatitaDb.instance () in
+ let similar = MetadataQuery.match_term ~dbd ty in
+ let convertible =
+ List.filter (
+ fun u ->
+ let t = CicUtil.term_of_uri u in
+ let ty',g =
+ CicTypeChecker.type_of_aux'
+ metasenv' [] t CicUniv.empty_ugraph
+ in
+ fst(CicReduction.are_convertible [] ty' ty g))
+ similar
+ in
+ (match convertible with
+ | [] -> ()
+ | x::_ ->
+ MatitaLog.warn
+ ("Theorem already proved: " ^ UriManager.string_of_uri x ^
+ "\nPlease use a variant."));
+ end;