aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.mlp
diff options
context:
space:
mode:
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