diff options
Diffstat (limited to 'grammar/q_util.mli')
| -rw-r--r-- | grammar/q_util.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/grammar/q_util.mli b/grammar/q_util.mli index f3af318b60..b163100fc3 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -50,3 +50,5 @@ val type_of_user_symbol : user_symbol -> argument_type val parse_user_entry : string -> string -> user_symbol val mlexpr_of_symbol : user_symbol -> MLast.expr + +val binders_of_tokens : MLast.expr -> extend_token list -> MLast.expr |