Abbreviation (u.4b72d9d53197f808b005effa2cda4f29.coq-core.8.20.1.doc.coq-core.interp.Abbreviation)

Source

val declare_abbreviation : 
  local:bool ->
  UserWarn.t option ->
  Names.Id.t ->
  onlyparsing:bool ->
  Notation_term.interpretation ->
  unit

Source

val search_abbreviation : 
  Globnames.abbreviation ->
  Notation_term.interpretation

Source

val search_filtered_abbreviation : 
  (Notation_term.interpretation -> 'a option) ->
  Globnames.abbreviation ->
  'a option

Sourceval import_abbreviation : int -> Libnames.full_path -> Names.KerName.t -> unit

Source

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

Source

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