NewDestruct/NewInduction acceptent l'option "using"

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

3 files changed, 24 insertions, 16 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2855118906..ef4d614612 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -237,6 +237,9 @@ GEXTEND Gram
       | "with"; l = LIST1 IDENT -> Some l
       | -> Some [] ] ]
   ;
+  eliminator:
+    [ [ "using"; el = constr_with_bindings -> el ] ]
+  ;
   simple_tactic:
     [ [ 
       (* Basic tactics *)
@@ -254,9 +257,8 @@ GEXTEND Gram
       | IDENT "Exact"; c = constr -> TacExact c
 
       | IDENT "Apply"; cl = constr_with_bindings -> TacApply cl
-      | IDENT "Elim"; cl = constr_with_bindings; "using";
-        el = constr_with_bindings -> TacElim (cl,Some el)
-      | IDENT "Elim"; cl = constr_with_bindings -> TacElim (cl,None)
+      | IDENT "Elim"; cl = constr_with_bindings; el = OPT eliminator ->
+          TacElim (cl,el)
       | IDENT "OldElim"; c = constr ->
 	  (* TacOldElim c *) error_oldelim ()
       | IDENT "ElimType"; c = constr -> TacElimType c
@@ -292,11 +294,13 @@ GEXTEND Gram
 
       (* Derived basic tactics *)
       | IDENT "Induction"; h = quantified_hypothesis -> TacOldInduction h
-      | IDENT "NewInduction"; c = induction_arg -> TacNewInduction c
+      | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator ->
+          TacNewInduction (c,el)
       | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "Destruct"; h = quantified_hypothesis -> TacOldDestruct h
-      | IDENT "NewDestruct"; c = induction_arg -> TacNewDestruct c
+      | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator ->
+          TacNewDestruct (c,el)
       | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
       | IDENT "Decompose"; IDENT "Sum"; c = constr -> TacDecomposeOr c
       | IDENT "Decompose"; "["; l = LIST1 qualid_or_ltac_ref; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index a448166e1c..e0f8bd3f1e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -303,6 +303,7 @@ let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) =
 
 let pr_bindings = pr_bindings pr_constr in
 let pr_with_bindings = pr_with_bindings pr_constr in
+let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_intarg n = spc () ++ int n in
 
@@ -339,10 +340,9 @@ and pr_atom1 = function
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
   | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
-  | TacElim (cb,None) -> hov 1 (str "Elim" ++ spc () ++ pr_with_bindings cb)
-  | TacElim (cb,Some cb') ->
+  | TacElim (cb,cbo) ->
       hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ 
-      spc () ++ str "using" ++ pr_arg pr_with_bindings cb')
+        pr_opt pr_eliminator cbo)
   | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c)
   | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
@@ -383,12 +383,14 @@ and pr_atom1 = function
   (* Derived basic tactics *)
   | TacOldInduction h ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction h ->
-      hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h)
+  | TacNewInduction (h,e) ->
+      hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
+        pr_opt pr_eliminator e)
   | TacOldDestruct h ->
       hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct h ->
-      hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h)
+  | TacNewDestruct (h,e) ->
+      hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
+        pr_opt pr_eliminator e)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "Double Induction" ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 8729dce067..ac97261065 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -355,12 +355,14 @@ let rec mlexpr_of_atomic_tactic = function
   (* Derived basic tactics *)
   | Tacexpr.TacOldInduction h ->
       <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewInduction c ->
-      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ >>
+  | Tacexpr.TacNewInduction (c,cbo) ->
+      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
+      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ >>
   | Tacexpr.TacOldDestruct h ->
       <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewDestruct c ->
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ >>
+  | Tacexpr.TacNewDestruct (c,cbo) ->
+      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
+      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ >>
 
   (* Context management *)
   | Tacexpr.TacClear l ->