let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
let local_names = List.map (fun (n,_) -> n) context in
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_term
- ~context ~metasenv ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ Disambiguate.disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+ ~initial_ugraph:() ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
~refine_thing:(refine_term status)
(text,prefix_len,
(initialize_ast ~universe ~lookup_in_library ~local_names term))
~visit:Disambiguate.bfvisit
- ~mk_localization_tbl ~expty ~subst
- in
- List.map (function (t,a,b,c,_) -> t,a,b,c) res, b
+ ~mk_localization_tbl
;;
-
let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- let obj' = initialize_obj ~universe ~lookup_in_library obj in
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_obj
- ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ let obj' = initialize_obj ~universe ~lookup_in_library obj in
+ Disambiguate.disambiguate_thing
+ ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe
- ~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+ ~initial_ugraph:() ~expty:None
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+ ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
(text,prefix_len,obj')
~visit:Disambiguate.bfvisit_obj
- ~mk_localization_tbl ~expty:None
- in
- List.map (function (o,a,b,c,_) -> o,a,b,c) res, b
+ ~mk_localization_tbl
;;
(*
let _ =