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.
---
 plugins/ltac/coretactics.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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