Utilisation de intro_pattern dans NewDestruct/NewInduction

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

4 files changed, 10 insertions, 14 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 225aa4728..3b7081012 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -236,7 +236,7 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids
+    [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
       | -> [] ] ]
   ;
   simple_tactic:
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 40a292ca1..c45dc332f 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -234,7 +234,7 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids
+    [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
       | -> [] ] ]
   ;
   simple_tactic:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9c23d0ba5..0382a2fdb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -130,24 +130,20 @@ let pr_bindings prc prlc = function
 let pr_with_bindings prc prlc (c,bl) = 
   prc c ++ hv 0 (pr_bindings prc prlc bl)
 
-let pr_with_names = function
-  | [] -> mt ()
-  | ids -> spc () ++ str "as [" ++
-      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
-              (prlist_with_sep spc pr_id) ids ++ str "]")
-
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
-(*
-  | IntroAndPattern pl ->
-      str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
-*)
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+
 let pr_hyp_location pr_id = function
   | InHyp id -> spc () ++ pr_id id
   | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index cf59d9a97..f5ebd8fcf 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -376,13 +376,13 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
   | Tacexpr.TacOldDestruct h ->
       <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
       <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)