let disambiguate_obj status obj =
let uri =
match obj with
- GrafiteAst.Inductive (_,(name,_,_,_)::_)
- | GrafiteAst.Record (_,name,_,_) ->
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) ->
Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
- | GrafiteAst.Inductive _ -> assert false
- | GrafiteAst.Theorem _ -> None in
+ | CicNotationPt.Inductive _ -> assert false
+ | CicNotationPt.Theorem _ -> None in
let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
if opts.do_heavy_checks then
begin
let dbd = MatitaDb.instance () in
- let similar = MetadataQuery.match_term ~dbd ty in
+ let similar = Whelp.match_term ~dbd ty in
let similar_len = List.length similar in
if similar_len> 30 then
(MatitaLog.message