Module Notgram_ops

Declare the parsing rules and entries of a (possibly uninterpreted) notation
val declare_notation_grammar : Constrexpr.notation -> Notation_gram.notation_grammar -> unit
val grammar_of_notation : Constrexpr.notation -> Notation_gram.notation_grammar

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