NewDestruct/NewInduction acceptent l'option "using"

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

5 files changed, 32 insertions, 19 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index f745570e9a..a5496f91d4 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 7a83eff5eb..6b4a1cbc15 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 71ec78b4c2..afc77834d2 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 572933eef8..2c589f07fa 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 9d1f616161..8dd0e34740 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. *)