aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.mli
diff options
context:
space:
mode:
authorGravatar Tej Chajed <tchajed@mit.edu>2017-02-16 10:24:15 -0500
committerGravatar Tej Chajed <tchajed@mit.edu>2017-02-16 13:49:11 -0500
commite6127d1f65a761a27c80b81c0f1bc5fca2b74af8 (patch)
tree9c839d3ef53da61f50a1c044d6120c3f5e363de8 /grammar/q_util.mli
parentbcb634d070519d6e37d9b7d39f12437a7d38f0c2 (diff)
[cleanup] Change Id.t option to Name.t in TacFun
Diffstat (limited to 'grammar/q_util.mli')
-rw-r--r--grammar/q_util.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index a5e36e47b..37ec1d56a 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -41,6 +41,8 @@ val mlexpr_of_string : string -> MLast.expr
val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
+val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr
+
val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
val type_of_user_symbol : user_symbol -> argument_type