3 files changed, 0 insertions, 42 deletions
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
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
 {
 
 open Pp
-open Constr
 open Stdarg
 open Pcoq.Prim
 open Pcoq.Constr
@@ -199,20 +198,6 @@ TACTIC EXTEND unify
 END
 
 {
-let deprecated_convert_concl_no_check =
-  CWarnings.create
-    ~name:"convert_concl_no_check" ~category:"deprecated"
-    (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
-}
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> {
-    deprecated_convert_concl_no_check ();
-    Tactics.convert_concl ~check:false x DEFAULTcast
-  }
-END
-
-{
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 0e5cac2d4a..74b0708743 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -19,12 +19,6 @@ let warn_deprecated_Spec =
     (fun () ->
       Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\"."))
 
-let warn_deprecated_Add =
-  CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated"
-    (fun () ->
-      Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>."))
-
-
 }
 
 DECLARE PLUGIN "zify_plugin"
@@ -41,17 +35,6 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
 | ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
 | ["Add" "Zify" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
 | ["Add" "Zify" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
-| ["Add" "InjTyp"    constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t }
-| ["Add" "BinOp"     constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t }
-| ["Add" "UnOp"      constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t }
-| ["Add" "CstOp"     constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t }
-| ["Add" "BinRel"    constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t }
-| ["Add" "PropOp"    constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t }
-| ["Add" "PropBinOp"    constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t }
-| ["Add" "PropUOp"   constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t }
-| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t }
-| ["Add" "UnOpSpec"  constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t }
-| ["Add" "Saturate"  constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t }
 END
 
 TACTIC EXTEND ITER
@@ -73,7 +56,4 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
 |[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
 |[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
 |[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
-|[ "Show" "Zify" "Spec"] -> {
-    warn_deprecated_Spec () ;
-    Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()}
 END