aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/genarg.ml5
-rw-r--r--interp/genarg.mli5
2 files changed, 10 insertions, 0 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 8eb8d2a0d6..0ed7b97f47 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -32,6 +32,7 @@ type argument_type =
| TacticArgType
| CastedOpenConstrArgType
| ConstrWithBindingsArgType
+ | WithBindingsArgType
| RedExprArgType
| List0ArgType of argument_type
| List1ArgType of argument_type
@@ -120,6 +121,10 @@ let rawwit_constr_with_bindings = ConstrWithBindingsArgType
let globwit_constr_with_bindings = ConstrWithBindingsArgType
let wit_constr_with_bindings = ConstrWithBindingsArgType
+let rawwit_with_bindings = WithBindingsArgType
+let globwit_with_bindings = WithBindingsArgType
+let wit_with_bindings = WithBindingsArgType
+
let rawwit_red_expr = RedExprArgType
let globwit_red_expr = RedExprArgType
let wit_red_expr = RedExprArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 6c4da92c76..2418646d9b 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -121,6 +121,10 @@ val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) ab
val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
+val rawwit_with_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
+val globwit_with_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_with_bindings : (constr bindings,constr,'ta) abstract_argument_type
+
val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
@@ -204,6 +208,7 @@ type argument_type =
| TacticArgType
| CastedOpenConstrArgType
| ConstrWithBindingsArgType
+ | WithBindingsArgType
| RedExprArgType
| List0ArgType of argument_type
| List1ArgType of argument_type