From cd17f9bfad72fb8f8da486facd75ff8ceecebd24 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 11:19:33 -0800
Subject: Remove double induction tactic

---
 plugins/ltac/coretactics.mlg | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
 | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
 END
 
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
-  { Elim.h_double_induction h1 h2 }
-END
-
 (* Admit *)
 
 TACTIC EXTEND admit
-- 
cgit v1.2.3