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 <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
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