diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 17:55:15 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 18:04:54 +0100 |
commit | f329e1e63eb29958c4cc0d7bddfdb84a754351d2 (patch) | |
tree | f05874effa8c32bad606e8a45599e9c52dd2e260 /grammar/q_util.mli | |
parent | f25396b3a35ea5cd64b8b68670e66a14a78c418c (diff) |
Do not keep the argument type in ExtNonTerminal.
Diffstat (limited to 'grammar/q_util.mli')
-rw-r--r-- | grammar/q_util.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 5f292baf3..c84e9d140 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *) type extend_token = | ExtTerminal of string -| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string +| ExtNonTerminal of Extend.user_symbol * string val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr |