Deprecate the destauto tactic

jfehrle · Jun 7, 2024 · 6bb096f · 6bb096f
1 parent d116fd0
commit 6bb096f
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/doc/changelog/04-tactics/19179-deprecate_destauto.rst b/doc/changelog/04-tactics/19179-deprecate_destauto.rst
@@ -0,0 +1,5 @@
+- **Deprecated:**
+  :tacn:`destauto`.
+  See `#11537 <https://github.com/coq/coq/issues/11537#issuecomment-2154260216>`_
+  (`#99999 <https://github.com/coq/coq/pull/99999>`_,
+  by Jim Fehrle).
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
@@ -482,9 +482,14 @@ TACTIC EXTEND specialize_eqs
 | [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id }
 END
 
+{
+let warn_destauto = CWarnings.create ~name:"destauto-deprecated" ~category:Deprecation.Version.v8_20
+    (fun () -> strbrk "The \"destauto\" tactic is deprecated.")
+}
+
 TACTIC EXTEND destauto
-| [ "destauto" ] -> { Internals.destauto }
-| [ "destauto" "in" hyp(id) ] -> { Internals.destauto_in id }
+| [ "destauto" ] -> { warn_destauto (); Internals.destauto }
+| [ "destauto" "in" hyp(id) ] -> { warn_destauto (); Internals.destauto_in id }
 END
 
 (**********************************************************************)