Notation_gramtype grammar_constr_prod_item = | GramConstrTerminal of bool * string |
| GramConstrNonTerminal of Extend.constr_prod_entry_key * Names.Id.t option |
| GramConstrListMark of int * bool * int |
Grammar rules for a notation
type one_notation_grammar = {notgram_level : Notation.level; |
notgram_assoc : Gramlib.Gramext.g_assoc option; |
notgram_notation : Constrexpr.notation; |
notgram_prods : grammar_constr_prod_item list list; |
notgram_typs : Extend.constr_entry_key list; |
}type notation_grammar = one_notation_grammar list