method set_disambiguate_status: #g_status -> 'self
end
-val eval_with_new_aliases:
+(* val eval_with_new_aliases:
#status as 'status -> ('status -> 'a) ->
- (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
+ ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list * 'a
+*)
-val set_proof_aliases:
+val get_interpr : db -> GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t
+
+val add_to_interpr:
+ #status as 'status ->
+ (Stdpp.location * GrafiteAst.alias_spec) list -> 'status
+
+val add_to_disambiguation_univ:
#status as 'status ->
- implicit_aliases:bool -> (* implicit ones are made explicit *)
- GrafiteAst.inclusion_mode ->
- (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
val aliases_for_objs:
#NCic.status -> NUri.uri list ->
#status as 'status ->
NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
- NotationPt.term * NCic.metasenv * NCic.substitution * 'status * NCic.term
+ NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
#status as 'status -> ?baseuri:string ->
(NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
- 'status * NCic.obj
+ 'status * NCic.obj
type pattern =
NotationPt.term Disambiguate.disambiguator_input option *