aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli5
2 files changed, 7 insertions, 0 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5920b0d508..64f8b3913e 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -59,6 +59,8 @@ let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
let wit_constr_with_bindings = make0 "constr_with_bindings"
+let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
+
let wit_bindings = make0 "bindings"
let wit_red_expr = make0 "redexpr"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index ac40a23281..893ec54d45 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -59,6 +59,11 @@ val wit_constr_with_bindings :
glob_constr_and_expr with_bindings,
constr with_bindings delayed_open) genarg_type
+val wit_open_constr_with_bindings :
+ (constr_expr with_bindings,
+ glob_constr_and_expr with_bindings,
+ constr with_bindings delayed_open) genarg_type
+
val wit_bindings :
(constr_expr bindings,
glob_constr_and_expr bindings,