- 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

7 files changed, 29 insertions, 18 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index aa0c3c771e..539b203d01 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -238,7 +238,7 @@ EXTEND
       [ e = argtype; LIDENT "list" -> List0ArgType e
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
-      [ e = LIDENT -> fst (interp_entry_name None e "")
+      [ e = LIDENT -> fst (interp_entry_name false None e "")
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -246,10 +246,10 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name None e "" in
+        let t, g = interp_entry_name false None e "" in
 	GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name None e sep in
+        let t, g = interp_entry_name false None e sep in
 	GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 99c6d8528c..b7928b3b54 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -652,26 +652,26 @@ let rec symbol_of_prod_entry_key = function
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
-let rec interp_entry_name up_level s sep =
+let rec interp_entry_name static up_level s sep =
   let l = String.length s in
   if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
     List1ArgType t, Alist1 g
   else if l > 12 & String.sub s 0 3 = "ne_" &
                    String.sub s (l-9) 9 = "_list_sep" then
-    let t, g = interp_entry_name up_level (String.sub s 3 (l-12)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
     List1ArgType t, Alist1sep (g,sep)
   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
     List0ArgType t, Alist0 g
   else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then
-    let t, g = interp_entry_name up_level (String.sub s 0 (l-9)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
     List0ArgType t, Alist0sep (g,sep)
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
     OptArgType t, Aopt g
   else if l > 5 & String.sub s (l-5) 5 = "_mods" then
-    let t, g = interp_entry_name up_level (String.sub s 0 (l-1)) "" in
+    let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
     List0ArgType t, Amodifiers g
   else
     let s = if s = "hyp" then "var" else s in
@@ -684,7 +684,10 @@ let rec interp_entry_name up_level s sep =
       try Some (get_entry uprim s), Aentry ("prim",s) with Not_found ->
       try Some (get_entry uconstr s), Aentry ("constr",s) with Not_found ->
       try Some (get_entry utactic s), Aentry ("tactic",s) with Not_found ->
-      None, Aentry ("",s) in
+	if static then
+	  error ("Unknown entry "^s^".")
+	else
+	  None, Aentry ("",s) in
     let t =
       match t with
 	| Some t -> type_of_typed_entry t
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 02db8d55d1..f356ae07e3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -270,8 +270,8 @@ val symbol_of_prod_entry_key :
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
-val interp_entry_name : int option -> string -> string -> 
-  entry_type * Gram.te prod_entry_key
+val interp_entry_name : bool (* true to fail on unknown entry *) ->
+  int option -> string -> string -> entry_type * Gram.te prod_entry_key
 
 (**********************************************************************)
 (* Registering/resetting the level of a constr entry                  *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index fc499241cf..d52ab8dd73 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -203,10 +203,10 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name None e "" in
+        let t, g = interp_entry_name false None e "" in
         GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name None e sep in
+        let t, g = interp_entry_name false None e sep in
         GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | s = STRING ->
 	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal.");
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index be9e0e422c..dd05d5cd76 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -82,10 +82,10 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name None e "" in
+        let t, g = interp_entry_name false None e "" in
         GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name None e sep in
+        let t, g = interp_entry_name false None e sep in
         GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | s = STRING ->
         GramTerminal s
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5342f961dc..88692a13c5 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 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 09b76d3f37..d085584264 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -47,7 +47,7 @@ let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, nt, po) ->
       let sep = match po with Some (_,sep) -> sep | _ -> "" in
-      let (etyp, e) = interp_entry_name (Some lev) nt sep in
+      let (etyp, e) = interp_entry_name true (Some lev) nt sep in
       GramNonTerminal (loc, etyp, e, Option.map fst po)
 
 let make_terminal_status = function