AbbreviationAbbreviations
val interp : data -> Notation_term.interpretationinterp a gives the interpretation of abbreviation a.
val full_path : data -> Libnames.full_pathfull_path a gives the full path of abbreviation a.
val enabled : data -> boolenabled a indicates whether the abbreviation a is enabled.
val only_parsing : data -> boolonly_parsing a indicates whether the abbreviation a is only used for parsing, and not for printing.
val fold : (Globnames.abbreviation -> data -> 'a -> 'a) -> 'a -> 'afold f acc folds function f over the current abbreviation map, using acc as the initial accumulator value.
val find_opt : Globnames.abbreviation -> data optionfind_opt k gives the abbreviation associated with the key k in the abbreviation map, if there is one.
val find_interp : Globnames.abbreviation -> Notation_term.interpretationfind_interp k gives the interpretation of the abbreviation associated with the key k in the abbreviation map. The Not_found exception is raised if k is not mapped.
val toggle : on:bool -> use:Notationextern.notation_use -> Globnames.abbreviation -> unittoggle ~on ~use key actives (if on) or deactivates (if not on) the abbreviation with the given key. An abbreviation associated with key should exist, otherwise Not_found is raised.
val toggle_if : on:bool -> use:Notationextern.notation_use -> (Globnames.abbreviation -> data -> bool) -> unittoggle_if ~on ~use pred is equivalent to running toggle ~on ~use on all abbreviations satisfying the given predicate pred.
val declare : local:Libobject.locality -> Globnames.extended_global_reference UserWarn.with_qf option -> Names.Id.t -> onlyparsing:bool -> Notation_term.interpretation -> unitval import : int -> Libnames.full_path -> Globnames.abbreviation -> unit