diff options
Diffstat (limited to 'intf/notation_term.ml')
| -rw-r--r-- | intf/notation_term.ml | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 084a1042c7..c342da3dca 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -88,12 +88,24 @@ type grammar_constr_prod_item = concat with last parsed list when true; additionally release the p last items as if they were parsed autonomously *) +(** Dealing with precedences *) + +type precedence = int +type parenRelation = L | E | Any | Prec of precedence +type tolerability = precedence * parenRelation + +type level = precedence * tolerability list * notation_var_internalization_type list + +(** Grammar rules for a notation *) + type one_notation_grammar = { - notgram_level : int; + notgram_level : level; notgram_assoc : Extend.gram_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; } -type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list +type notation_grammar = { + notgram_onlyprinting : bool; + notgram_rules : one_notation_grammar list +} |