aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-15 22:30:09 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-16 12:17:39 +0200
commitcd3971e53b76cb62e14822eb3e275d3968a4f215 (patch)
treedc2bdaa617d1bd30209ae63083c9e4d7d392917d /grammar/q_util.mli
parent9f8220164703aee47c6c6d7dba07caabf7555c1c (diff)
Adding support for using grammar entries returning no value in EXTEND.
Diffstat (limited to 'grammar/q_util.mli')
-rw-r--r--grammar/q_util.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5b3eb3202..0b3def058 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -23,7 +23,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr