aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.mlp
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.mlp
parent9f8220164703aee47c6c6d7dba07caabf7555c1c (diff)
Adding support for using grammar entries returning no value in EXTEND.
Diffstat (limited to 'grammar/q_util.mlp')
-rw-r--r--grammar/q_util.mlp2
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 8b930cf36..87262e1c8 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -25,7 +25,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
let mlexpr_of_list f l =
List.fold_right