Merge PR coq#19129: Deprecate the gintuition tactic.

Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · Jun 3, 2024 · 2e621ae · 2e621ae
2 parents 4248ee4 + abeaa79
commit 2e621ae
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/doc/changelog/04-tactics/19129-deprecate-gintuition.rst 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 <https://github.com/coq/coq/pull/19129>`_,
+  by Pierre-Marie Pédrot).
diff --git 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
@@ -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