aboutsummaryrefslogtreecommitdiff
path: root/parsing/notation_gram.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-04-01 12:51:16 +0200
committerPierre-Marie Pédrot2019-04-01 12:51:16 +0200
commitd16633368ba33d05bcae3e98b1e05efc5f530206 (patch)
tree4cd4f1c348a7e0a5d90a91c2b9a61ab91672cb73 /parsing/notation_gram.ml
parent4c3f4d105a32cc7661ae714fe4e25619e32bc84c (diff)
parentd8d3b7a8251b874c436ac11b881cf4fb5f991784 (diff)
Merge PR #9815: Multiple payload types in tokens
Reviewed-by: ppedrot Ack-by: proux01
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;