From 3466c08689439804e828f7b809e698346fa76a3b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Sep 2020 12:18:24 +0200
Subject: Formally deprecate the double induction tactic.

The doc states it is deprecated since 1386cd9 but this was ages before the
deprecation mechanism existed.
---
 test-suite/success/induct.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3