package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Declare the parsing rules and entries of a (possibly uninterpreted) notation
val declare_notation_grammar : Constrexpr.notation -> Notation_gram.notation_grammar -> unit

raise Not_found if not declared

val declare_notation_subentries : Constrexpr.notation -> Extend.constr_entry_key list -> unit
val subentries_of_notation : Constrexpr.notation -> Extend.constr_entry_key list
val get_defined_notations : unit -> Constrexpr.notation list

Returns notations with defined parsing/printing rules