Interprétation des listes de VarArgType dans les notations faisant

référence à des arguments génériques



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9839 85f007b7-540e-0410-9357-904b9bb8a0f7

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 =