package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : ?loc:Loc.t -> Globnames.abbreviation -> Notation_term.interpretation
val search_filtered_abbreviation : ?loc:Loc.t -> (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

OCaml

Innovation. Community. Security.