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

raise Not_found if not declared

val declare_notation_non_terminals : Constrexpr.notation -> Extend.constr_entry_key list -> unit
val non_terminals_of_notation : Constrexpr.notation -> Extend.constr_entry_key list
val longest_common_prefix : Constrexpr.notation -> (Constrexpr.notation * int) option

longest_common_prefix ntn looks among notations ntn' already registered with declare_notation_non_terminals ntn' for the one that shares the longest common prefix with ntn, if any returns Some (ntn', k) where k is the number of nonterminal symbols in the common prefix between ntn and ntn'.

val get_defined_notations : unit -> Constrexpr.notation list

Returns notations with defined parsing/printing rules