diff options
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b0e8d7322e..4dfcebbe7c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1850,6 +1850,8 @@ and interp_genarg ist gl x = (interp_bindings ist gl (out_gen globwit_bindings x)) | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x + | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x + | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x | List0ArgType _ -> app_list0 (interp_genarg ist gl) x | List1ArgType _ -> app_list1 (interp_genarg ist gl) x | OptArgType _ -> app_opt (interp_genarg ist gl) x @@ -1872,6 +1874,16 @@ and interp_genarg_constr_list1 ist gl x = let lc = pf_interp_constr_list ist gl lc in in_gen (wit_list1 wit_constr) lc +and interp_genarg_var_list0 ist gl x = + let lc = out_gen (wit_list0 globwit_var) x in + let lc = interp_hyp_list ist gl lc in + in_gen (wit_list0 wit_var) lc + +and interp_genarg_var_list1 ist gl x = + let lc = out_gen (wit_list1 globwit_var) x in + let lc = interp_hyp_list ist gl lc in + in_gen (wit_list1 wit_var) lc + (* Interprets the Match expressions *) and interp_match ist g lz constr lmr = let rec apply_match_subterm ist nocc (id,c) csr mt = |