diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 488e8833cc..3434299ab0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -821,9 +821,9 @@ and intern_genarg ist x = | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) - | WithBindingsArgType -> - in_gen globwit_with_bindings - (intern_bindings ist (out_gen rawwit_with_bindings x)) + | BindingsArgType -> + in_gen globwit_bindings + (intern_bindings ist (out_gen rawwit_bindings x)) | List0ArgType _ -> app_list0 (intern_genarg ist) x | List1ArgType _ -> app_list1 (intern_genarg ist) x | OptArgType _ -> app_opt (intern_genarg ist) x @@ -1533,9 +1533,9 @@ and interp_genarg ist goal x = | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x)) - | WithBindingsArgType -> - in_gen wit_with_bindings - (interp_bindings ist goal (out_gen globwit_with_bindings x)) + | BindingsArgType -> + in_gen wit_bindings + (interp_bindings ist goal (out_gen globwit_bindings x)) | List0ArgType _ -> app_list0 (interp_genarg ist goal) x | List1ArgType _ -> app_list1 (interp_genarg ist goal) x | OptArgType _ -> app_opt (interp_genarg ist goal) x @@ -1728,7 +1728,7 @@ and interp_atomic ist gl = function | QuantHypArgType | RedExprArgType | TacticArgType -> val_interp ist gl (out_gen globwit_tactic x) - | CastedOpenConstrArgType | ConstrWithBindingsArgType | WithBindingsArgType + | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ -> error "This generic type is not supported in alias" in @@ -2017,9 +2017,9 @@ and subst_genarg subst (x:glob_generic_argument) = | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x)) - | WithBindingsArgType -> - in_gen globwit_with_bindings - (subst_bindings subst (out_gen globwit_with_bindings x)) + | BindingsArgType -> + in_gen globwit_bindings + (subst_bindings subst (out_gen globwit_bindings x)) | List0ArgType _ -> app_list0 (subst_genarg subst) x | List1ArgType _ -> app_list1 (subst_genarg subst) x | OptArgType _ -> app_opt (subst_genarg subst) x |