NewDestruct/NewInduction acceptent l'option "using"

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

10 files changed, 59 insertions, 37 deletions

diff --git a/CHANGES b/CHANGES
index 755eab9ca..1519fca56 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,6 +50,7 @@ Tactics
 - "Inversion" now applies also on quantified hypotheses (naming as
   for Intros until)
 - NewDestruct now accepts terms with missing hypotheses
+- NewDestruct and NewInduction now accept user-provided elimination scheme
 - Omega could solve goals such as ~`x<y` |- `x>=y` but failed when the
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 285511890..ef4d61461 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 a448166e1..e0f8bd3f1 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 8729dce06..ac9726106 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 ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b63588aaa..3eaaea573 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -116,9 +116,9 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
 
   (* Derived basic tactics *)
   | TacOldInduction of quantified_hypothesis
-  | TacNewInduction of 'constr induction_arg
+  | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
   | TacOldDestruct of quantified_hypothesis
-  | TacNewDestruct of 'constr induction_arg
+  | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index f745570e9..a5496f91d 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -52,8 +52,10 @@ let h_instantiate n c =
 (* Derived basic tactics *)
 let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h)
 let h_old_destruct h  = abstract_tactic (TacOldDestruct h) (old_destruct h)
-let h_new_induction c = abstract_tactic (TacNewInduction c) (new_induct c)
-let h_new_destruct c = abstract_tactic (TacNewDestruct c) (new_destruct c)
+let h_new_induction c e =
+  abstract_tactic (TacNewInduction (c,e)) (new_induct c e)
+let h_new_destruct c e =
+  abstract_tactic (TacNewDestruct (c,e)) (new_destruct c e)
 let h_specialize n (c,bl as d) =
   abstract_tactic (TacSpecialize (n,d)) (new_hyp n c bl)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 7a83eff5e..6b4a1cbc1 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -55,8 +55,10 @@ val h_instantiate     : int -> constr -> tactic
 
 val h_old_induction   : quantified_hypothesis -> tactic
 val h_old_destruct    : quantified_hypothesis -> tactic
-val h_new_induction   : constr induction_arg -> tactic
-val h_new_destruct    : constr induction_arg -> tactic
+val h_new_induction   :
+  constr induction_arg -> constr with_bindings option -> tactic
+val h_new_destruct    :
+  constr induction_arg -> constr with_bindings option -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71ec78b4c..afc77834d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -503,9 +503,13 @@ let rec glob_atomic lf ist = function
 
   (* Derived basic tactics *)
   | TacOldInduction h -> TacOldInduction (glob_quantified_hypothesis ist h)
-  | TacNewInduction c -> TacNewInduction (glob_induction_arg ist c)
+  | TacNewInduction (c,cbo) ->
+      TacNewInduction (glob_induction_arg ist c,
+               option_app (glob_constr_with_bindings ist) cbo)
   | TacOldDestruct h -> TacOldDestruct (glob_quantified_hypothesis ist h)
-  | TacNewDestruct c -> TacNewDestruct (glob_induction_arg ist c)
+  | TacNewDestruct (c,cbo) ->
+      TacNewDestruct (glob_induction_arg ist c,
+               option_app (glob_constr_with_bindings ist) cbo)
   | TacDoubleInduction (h1,h2) ->
       let h1 = glob_quantified_hypothesis ist h1 in
       let h2 = glob_quantified_hypothesis ist h2 in
@@ -1634,9 +1638,13 @@ and interp_atomic ist = function
 
   (* Derived basic tactics *)
   | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist h)
-  | TacNewInduction c -> h_new_induction (interp_induction_arg ist c)
+  | TacNewInduction (c,cbo) ->
+      h_new_induction (interp_induction_arg ist c)
+        (option_app (interp_constr_with_bindings ist) cbo)
   | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist h)
-  | TacNewDestruct c -> h_new_destruct (interp_induction_arg ist c)
+  | TacNewDestruct (c,cbo) -> 
+      h_new_destruct (interp_induction_arg ist c)
+        (option_app (interp_constr_with_bindings ist) cbo)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 572933eef..2c589f07f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1335,32 +1335,33 @@ let induction_from_context isrec style elim hyp0 gl =
     ]
     gl
 
-let induction_with_atomization_of_ind_arg isrec hyp0 =
+let induction_with_atomization_of_ind_arg isrec elim hyp0 =
   tclTHEN
     (atomize_param_of_ind hyp0)
-    (induction_from_context isrec false None hyp0)
+    (induction_from_context isrec false elim hyp0)
 
 (* This is Induction since V7 ("natural" induction both in quantified
    premisses and introduced ones) *)
-let new_induct_gen isrec c gl =
+let new_induct_gen isrec elim c gl =
   match kind_of_term c with
     | Var id when not (mem_named_context id (Global.named_context())) ->
-	induction_with_atomization_of_ind_arg isrec id gl
+	induction_with_atomization_of_ind_arg isrec elim id gl
     | _        ->
 	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) 
 		  Anonymous in
 	let id = fresh_id [] x gl in
 	tclTHEN
 	  (letin_tac true (Name id) c (None,[]))
-	  (induction_with_atomization_of_ind_arg isrec id) gl
+	  (induction_with_atomization_of_ind_arg isrec elim id) gl
 
-let new_induct_destruct isrec = function
-  | ElimOnConstr c -> new_induct_gen isrec c
+let new_induct_destruct isrec c elim = match c with
+  | ElimOnConstr c -> new_induct_gen isrec elim c
   | ElimOnAnonHyp n ->
-      tclTHEN (intros_until_n n) (tclLAST_HYP (new_induct_gen isrec))
+      tclTHEN (intros_until_n n) (tclLAST_HYP (new_induct_gen isrec elim))
   (* Identifier apart because id can be quantified in goal and not typable *)
   | ElimOnIdent (_,id) ->
-      tclTHEN (tclTRY (intros_until_id id)) (new_induct_gen isrec (mkVar id))
+      tclTHEN (tclTRY (intros_until_id id))
+        (new_induct_gen isrec elim (mkVar id))
 
 let new_induct = new_induct_destruct true
 let new_destruct = new_induct_destruct false
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9d1f61616..8dd0e3474 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -171,7 +171,7 @@ val old_induct     : quantified_hypothesis -> tactic
 val general_elim_in : identifier -> constr * constr substitution ->
                       constr * constr substitution -> tactic
 
-val new_induct     : constr induction_arg -> tactic
+val new_induct : constr induction_arg -> constr with_bindings option -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -179,7 +179,7 @@ val general_case_analysis : constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val old_destruct          : quantified_hypothesis -> tactic
-val new_destruct          : constr induction_arg -> tactic
+val new_destruct : constr induction_arg -> constr with_bindings option ->tactic
 
 (*s Eliminations giving the type instead of the proof. *)