From abeaa79a1d886b4f98bc09a78f8f4efedc3eeebc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sat, 1 Jun 2024 23:19:18 +0200 Subject: [PATCH] Deprecate the gintuition tactic. It used to be a hidden tactic, that was only documented after #15265 in Coq 8.16. It is neither used in the test-suite nor in the CI, so it is a perfect candidate for quick removal. --- doc/changelog/04-tactics/19129-deprecate-gintuition.rst | 5 +++++ doc/sphinx/proofs/automatic-tactics/logic.rst | 2 ++ plugins/firstorder/g_ground.mlg | 2 +- 3 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/04-tactics/19129-deprecate-gintuition.rst diff --git a/doc/changelog/04-tactics/19129-deprecate-gintuition.rst b/doc/changelog/04-tactics/19129-deprecate-gintuition.rst new file mode 100644 index 000000000000..75c1c50339a2 --- /dev/null +++ b/doc/changelog/04-tactics/19129-deprecate-gintuition.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + the :tacn:`gintuition` tactic, which used to be undocumented + until Coq 8.16 + (`#19129 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 67439f27e133..dc417eb104ab 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -148,6 +148,8 @@ Solvers for logic and equality .. tacn:: gintuition {? @ltac_expr } + .. deprecated:: 8.20 + An extension of :tacn:`intuition` to first-order reasoning (similar to how :tacn:`firstorder` extends :tacn:`tauto`). diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 3306126c33aa..18a76c93f3f0 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -129,7 +129,7 @@ TACTIC EXTEND firstorder { gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' } END -TACTIC EXTEND gintuition +TACTIC EXTEND gintuition DEPRECATED { Deprecation.make ~since:"8.20" () } | [ "gintuition" tactic_opt(t) ] -> { gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] } END