Merge PR #13764: Remove Add InjTyp and 10 other micromega commands (deprecated in 8.13)

Reviewed-by: Zimmi48
Reviewed-by: fajb

3 files changed, 6 insertions, 82 deletions

diff --git a/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst
new file mode 100644
index 0000000000..fc6c88eab6
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  `Show Zify Spec`, `Add InjTyp` and 11 similar `Add *` commands.
+  For `Show Zify Spec`, use `Show Zify UnOpSpec` or `Show Zify BinOpSpec` instead.
+  For `Add *`, `Use Add Zify *` intead of `Add *`
+  (`#13764 <https://github.com/coq/coq/pull/13764>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 38c4886e0f..3bd85d29c8 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -315,68 +315,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    prints the list of types that supported by :tacn:`zify` i.e.,
    :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. cmd:: Show Zify Spec
-
-   .. deprecated:: 8.13
-       Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead.
-
-.. cmd:: Add InjTyp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``InjTyp`` instead.
-
-.. cmd:: Add BinOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinOp`` instead.
-
-.. cmd:: Add BinOpSpec @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinOpSpec`` instead.
-
-.. cmd:: Add UnOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``UnOp`` instead.
-
-.. cmd:: Add UnOpSpec @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``UnOpSpec`` instead.
-
-.. cmd:: Add CstOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``CstOp`` instead.
-
-.. cmd:: Add BinRel @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinRel`` instead.
-
-.. cmd:: Add PropOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropOp`` instead.
-
-.. cmd:: Add PropBinOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropBinOp`` instead.
-
-.. cmd:: Add PropUOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropUOp`` instead.
-
-.. cmd:: Add Saturate @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``Saturate`` instead.
-
-
-
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#fnpsatz] Variants deal with equalities and strict inequalities.
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