diff options
Diffstat (limited to 'intf/notation_term.ml')
| -rw-r--r-- | intf/notation_term.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cee96040b..084a1042c 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -88,11 +88,12 @@ type grammar_constr_prod_item = concat with last parsed list when true; additionally release the p last items as if they were parsed autonomously *) -type notation_grammar = { +type one_notation_grammar = { notgram_level : int; 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; - notgram_onlyprinting : bool; } + +type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list |