aboutsummaryrefslogtreecommitdiff
path: root/parsing/notation_gram.ml
diff options
context:
space:
mode:
authorPierre Roux2019-02-17 10:10:22 +0100
committerPierre Roux2019-03-31 23:17:55 +0200
commiteadb00648127c9a535b533d51189dce41ef16db7 (patch)
tree1e5db53e73950ca4c7d7d9ae5e01a5d5c83ac32f /parsing/notation_gram.ml
parent5dd3c18f4e50eef53ae4413b7b80951f17edad5f (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.ml2
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;