diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 962deff27e5f..4ab16faf4402 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -188,11 +188,9 @@ described elsewhere
       .. insertprodn logical_kind logical_kind
 
       .. prodn::
-         logical_kind ::= Fixpoint
-         | CoFixpoint
-         | {| @thm_token | @assumption_token }
+         logical_kind ::= {| @thm_token | @assumption_token }
          | {| Definition | Example | Context | Primitive | Symbol }
-         | {| Coercion | Instance | Scheme | Canonical | SubClass }
+         | {| Coercion | Instance | Scheme | Canonical | SubClass | Fixpoint | CoFixpoint }
          | {| Field | Method }
 
       Filters objects by the keyword that was used to define them
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index b651857600ea..91bdb023214b 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1971,7 +1971,9 @@ logical_kind: [
 | DELETE "Instance"
 | DELETE "Scheme"
 | DELETE "Canonical"
-| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| DELETE "Fixpoint"
+| DELETE "CoFixpoint"
+| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" | "Fixpoint" | "CoFixpoint" ]
 | DELETE "Field"
 | DELETE "Method"
 | [ "Field" | "Method" ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aa307a941ae1..3ba8c38a5625 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1053,11 +1053,9 @@ search_item: [
 ]
 
 logical_kind: [
-| "Fixpoint"
-| "CoFixpoint"
 | [ thm_token | assumption_token ]
 | [ "Definition" | "Example" | "Context" | "Primitive" | "Symbol" ]
-| [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" | "Fixpoint" | "CoFixpoint" ]
 | [ "Field" | "Method" ]
 ]