Merge PR #12963: Formally deprecate the double induction tactic.

Reviewed-by: VincentSe
Ack-by: herbelin
Ack-by: olaure01

3 files changed, 9 insertions, 20 deletions

diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index cb226de586..f1f538ab39 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -263,7 +263,7 @@ END
 
 (** Double induction *)
 
-TACTIC EXTEND double_induction
+TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
 | [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
   { Elim.h_double_induction h1 h2 }
 END
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index a39b17e1f1..4983ee3c0d 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -159,6 +159,8 @@ Abort.
 (* This was failing in 8.5 and before because of a bug in the order of
    hypotheses *)
 
+Set Warnings "-deprecated".
+
 Inductive I2 : Type :=
   C2 : forall x:nat, x=x -> I2.
 Goal forall a b:I2, a = b.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 015eb8e2ac..7238ec0068 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -78,25 +78,12 @@ Section sequence.
   Lemma growing_prop :
     forall n m:nat, Un_growing -> (n >= m)%nat -> Un n >= Un m.
   Proof.
-    double induction n m; intros.
-    unfold Rge; right; trivial.
-    exfalso; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
-    cut (n0 >= 0)%nat.
-    generalize H0; intros; unfold Un_growing in H0;
-      apply
-        (Rge_trans (Un (S n0)) (Un n0) (Un 0) (Rle_ge (Un n0) (Un (S n0)) (H0 n0))
-          (H 0%nat H2 H3)).
-    elim n0; auto.
-    elim (lt_eq_lt_dec n1 n0); intro y.
-    elim y; clear y; intro y.
-    unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro;
-      exfalso; auto.
-    rewrite y; unfold Rge; right; trivial.
-    unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro;
-      unfold Un_growing in H1;
-        apply
-          (Rge_trans (Un (S n1)) (Un n1) (Un (S n0))
-            (Rle_ge (Un n1) (Un (S n1)) (H1 n1)) H3).
+    intros * Hgrowing Hle.
+    induction Hle as [|p].
+    - apply Rge_refl.
+    - apply Rge_trans with (Un p).
+      + apply Rle_ge, Hgrowing.
+      + apply IHHle.
   Qed.
 
 (*********)