diff options
| author | Pierre Roux | 2019-02-17 10:10:22 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-03-31 23:17:55 +0200 |
| commit | eadb00648127c9a535b533d51189dce41ef16db7 (patch) | |
| tree | 1e5db53e73950ca4c7d7d9ae5e01a5d5c83ac32f /parsing/notation_gram.ml | |
| parent | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (diff) | |
Multiple payload types in tokens
Instead of just string (and empty strings for tokens without payload)
Diffstat (limited to 'parsing/notation_gram.ml')
| -rw-r--r-- | parsing/notation_gram.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index a50f8d69e3..6df0d6f21a 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -21,7 +21,7 @@ type level = Constrexpr.notation_entry * precedence * tolerability list * constr (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = - | GramConstrTerminal of Tok.pattern + | GramConstrTerminal of string Tok.p | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option | GramConstrListMark of int * bool * int (* tells action rule to make a list of the n previous parsed items; |
