diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 8 | ||||
| -rw-r--r-- | interp/genarg.mli | 10 |
2 files changed, 9 insertions, 9 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 0ed7b97f47..80248f7e5e 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -32,7 +32,7 @@ type argument_type = | TacticArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType - | WithBindingsArgType + | BindingsArgType | RedExprArgType | List0ArgType of argument_type | List1ArgType of argument_type @@ -121,9 +121,9 @@ 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_bindings = BindingsArgType +let globwit_bindings = BindingsArgType +let wit_bindings = BindingsArgType let rawwit_red_expr = RedExprArgType let globwit_red_expr = RedExprArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index 2418646d9b..23e1b5377d 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -60,7 +60,7 @@ ConstrMayEvalArgType constr_expr may_eval constr QuantHypArgType quantified_hypothesis quantified_hypothesis TacticArgType raw_tactic_expr tactic CastedOpenConstrArgType constr_expr open_constr -ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings +ConstrBindingsArgType constr_expr with_bindings constr with_bindings List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type @@ -121,9 +121,9 @@ 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_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type +val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type +val wit_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 @@ -208,7 +208,7 @@ type argument_type = | TacticArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType - | WithBindingsArgType + | BindingsArgType | RedExprArgType | List0ArgType of argument_type | List1ArgType of argument_type |