diff options
Diffstat (limited to 'parsing/notation_gram.ml')
| -rw-r--r-- | parsing/notation_gram.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 9f133ca9d4..ffc92fa53a 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -37,7 +37,4 @@ type one_notation_grammar = { notgram_prods : grammar_constr_prod_item list list; } -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} +type notation_grammar = one_notation_grammar list |