- disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
- ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term
- ~interpretate_thing:interpretate_term ~refine_thing:refine_term term
-
- let disambiguate_obj ~dbd ~aliases ~uri obj =
- disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
- ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
- ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
- obj
+ let term =
+ if fresh_instances then CicNotationUtil.freshen_term term else term
+ in
+ disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
+ ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
+ ~refine_thing:refine_term term
+
+ let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj =
+ let obj =
+ if fresh_instances then CicNotationUtil.freshen_obj obj else obj
+ in
+ disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
+ ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
+ ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
+ obj