assert (uri = None);
let rec aux ~localize loc (context: Cic.name list) = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
assert (uri = None);
let rec aux ~localize loc (context: Cic.name list) = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
match indty_ident with
| Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
match indty_ident with
| Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
let localization_tbl = Cic.CicHash.create 23 in
(* here we are throwing away useful localization informations!!! *)
fst (
let localization_tbl = Cic.CicHash.create 23 in
(* here we are throwing away useful localization informations!!! *)
fst (
path ~localization_tbl, localization_tbl)
let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
path ~localization_tbl, localization_tbl)
let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term
~refine_thing:refine_term (text,prefix_len,term)
let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
~refine_thing:refine_term (text,prefix_len,term)
let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri