From 7a7efb875386ce297f54afb9754619a7c4e8090a Mon Sep 17 00:00:00 2001 From: Pierre Rousselin <119015057+Villetaneuse@users.noreply.github.com> Date: Thu, 16 May 2024 11:40:14 +0200 Subject: [PATCH] Update doc/tools/docgram/common.edit_mlg Co-authored-by: Jim Fehrle --- doc/sphinx/proof-engine/vernacular-commands.rst | 4 ++-- doc/tools/docgram/common.edit_mlg | 4 ++-- doc/tools/docgram/orderedGrammar | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4ab16faf4402..47e038df26c8 100644 --- 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 index 91bdb023214b..917be045d7cb 100644 --- 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 index 3ba8c38a5625..2cf33cfa8f06 100644 --- 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: [