diff options
| author | Hugo Herbelin | 2019-10-05 22:07:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-21 18:49:31 +0100 |
| commit | d8dc892dc4e50462163053124c9bafcd312433a5 (patch) | |
| tree | ac389a9bcdc6444296d89aa2af1ad113c014dde2 /parsing/notation_gram.ml | |
| parent | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (diff) | |
Notations: Avoiding computing parsing rule when in onlyprinting mode.
In particular, this fixes #9741.
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 |