Update documented syntax

Villetaneuse · Apr 27, 2024 · d40e0aa · d40e0aa
1 parent df038c9
commit d40e0aa
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 1 deletion.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -188,7 +188,9 @@ described elsewhere
       .. insertprodn logical_kind logical_kind
 
       .. prodn::
-         logical_kind ::= {| @thm_token | @assumption_token }
+         logical_kind ::= Fixpoint
+         | CoFixpoint
+         | {| @thm_token | @assumption_token }
          | {| Definition | Example | Context | Primitive | Symbol }
          | {| Coercion | Instance | Scheme | Canonical | SubClass }
          | {| Field | Method }

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -1516,6 +1516,8 @@ logical_kind: [
 extended_def_token: [
 | def_token
 | "Coercion"
+| "Fixpoint"
+| "CoFixpoint"
 | "Instance"
 | "Scheme"
 | "Canonical"

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -1053,6 +1053,8 @@ search_item: [
 ]
 
 logical_kind: [
+| "Fixpoint"
+| "CoFixpoint"
 | [ thm_token | assumption_token ]
 | [ "Definition" | "Example" | "Context" | "Primitive" | "Symbol" ]
 | [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]