Update doc/tools/docgram/common.edit_mlg

Co-authored-by: Jim Fehrle <[email protected]>
Villetaneuse · May 16, 2024 · 7a7efb8 · 7a7efb8
1 parent 8dbbcd6
commit 7a7efb8
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -190,8 +190,8 @@ described elsewhere
       .. prodn::
          logical_kind ::= {| @thm_token | @assumption_token }
          | {| Definition | Example | Context | Primitive | Symbol }
-         | {| Coercion | Instance | Scheme | Canonical | SubClass | Fixpoint | CoFixpoint }
-         | {| Field | Method }
+         | {| Coercion | Instance | Scheme | Canonical | SubClass }
+         | {| Fixpoint | CoFixpoint | Field | Method }
 
       Filters objects by the keyword that was used to define them
       (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`,

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
@@ -1971,12 +1971,12 @@ 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" ]
+| [  "Fixpoint" | "CoFixpoint" | "Field" | "Method" ]
 ]
 
 (* ltac2 *)

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