- 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
(DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
(* args: print function, message (may be empty), status *)
val dump_aliases: (string -> unit) -> string -> #status -> unit
(DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
(* args: print function, message (may be empty), status *)
val dump_aliases: (string -> unit) -> string -> #status -> unit
exception BaseUriNotSetYet
val disambiguate_nterm :
#status as 'status ->
NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
exception BaseUriNotSetYet
val disambiguate_nterm :
#status as 'status ->
NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
val disambiguate_nobj :
#status as 'status -> ?baseuri:string ->
(NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
val disambiguate_nobj :
#status as 'status -> ?baseuri:string ->
(NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
type pattern =
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
val disambiguate_npattern:
type pattern =
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
val disambiguate_npattern: