package coq

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

Syntactic definitions.

val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Names.Id.t -> onlyparsing:bool -> Notation_term.interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> Names.KerName.t -> Notation_term.interpretation
val search_filtered_syntactic_definition : ?loc:Loc.t -> (Notation_term.interpretation -> 'a option) -> Names.KerName.t -> 'a option
val import_syntax_constant : int -> Libnames.full_path -> Names.KerName.t -> unit