Abbreviation
Abbreviations.
val declare_abbreviation :
local:bool ->
?also_in_cases_pattern:bool ->
Deprecation.t option ->
Names.Id.t ->
onlyparsing:bool ->
Notation_term.interpretation ->
unit
val search_abbreviation :
Globnames.abbreviation ->
Notation_term.interpretation
val search_filtered_abbreviation :
( Notation_term.interpretation -> 'a option ) ->
Globnames.abbreviation ->
'a option
val import_abbreviation : int -> Libnames.full_path -> Names.KerName.t -> unit
val toggle_abbreviation :
on:bool ->
use:Notationextern.notation_use ->
Globnames.abbreviation ->
unit
Activate (if on:true) or deactivate (if on:false) an abbreviation assumed to exist
val toggle_abbreviations :
on:bool ->
use:Notationextern.notation_use ->
( Libnames.full_path -> Notation_term.interpretation -> bool ) ->
unit
Activate (if on:true) or deactivate (if on:false) all abbreviations satisfying a criterion