diff options
| author | Pierre-Marie Pédrot | 2020-09-01 12:18:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-17 08:07:59 +0200 |
| commit | 3466c08689439804e828f7b809e698346fa76a3b (patch) | |
| tree | 110a13095774ed47b2d8547831d724357299d468 /test-suite | |
| parent | 3ff6af396ce73291a127707022aa2c96adc52b0b (diff) | |
Formally deprecate the double induction tactic.
The doc states it is deprecated since 1386cd9 but this was ages before the
deprecation mechanism existed.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/induct.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |