- Fixed a little bug in previous commit (bad failure in case of unknown entry).

- Added support for list of intropattern in Tactic Notation.



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

1 files changed, 8 insertions, 0 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5342f961d..88692a13c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2420,6 +2420,10 @@ and interp_atomic ist gl = function
         let wit = wit_list0 (globwit_ident_gen b) in
 	let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in
         VList (List.map mk_ident (out_gen wit x))
+    | List0ArgType IntroPatternArgType -> 
+        let wit = wit_list0 globwit_intro_pattern in
+	let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
+        VList (List.map mk_ipat (out_gen wit x))
     | List1ArgType ConstrArgType -> 
         let wit = wit_list1 globwit_constr in
         VList (List.map (mk_constr_value ist gl) (out_gen wit x))
@@ -2436,6 +2440,10 @@ and interp_atomic ist gl = function
         let wit = wit_list1 (globwit_ident_gen b) in
 	let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in
         VList (List.map mk_ident (out_gen wit x))
+    | List1ArgType IntroPatternArgType -> 
+        let wit = wit_list1 globwit_intro_pattern in
+	let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
+        VList (List.map mk_ipat (out_gen wit x))
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
     | OpenConstrArgType _ | ConstrWithBindingsArgType