Update refman's Search documentation

Villetaneuse · Apr 28, 2024 · 3141a8d · 3141a8d
1 parent ab6d31f
commit 3141a8d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 deletions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -188,18 +188,17 @@ described elsewhere
       .. insertprodn logical_kind logical_kind
 
       .. prodn::
-         logical_kind ::= Fixpoint
-         | CoFixpoint
+         logical_kind ::=
          | {| @thm_token | @assumption_token }
          | {| Definition | Example | Context | Primitive | Symbol }
-         | {| Coercion | Instance | Scheme | Canonical | SubClass }
+         | {| FixPoint | CoFixpoint | Coercion | Instance | Scheme | Canonical | SubClass }
          | {| Field | Method }
 
       Filters objects by the keyword that was used to define them
       (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`,
       `Primitive`...) or its status (`Coercion`, `Instance`, `Scheme`,
-      `Canonical`, `SubClass`, Field` for record fields, `Method` for class
-      fields).  Note that `Coercion`\s, `Canonical Structure`\s, Instance`\s and `Scheme`\s can be
+      `Canonical`, `SubClass`, `Field` for record fields, `Method` for class
+      fields).  Note that `Coercion`\s, `Canonical Structure`\s, `Instance`\s and `Scheme`\s can be
       defined without using those keywords.  See :ref:`this example <search-by-keyword>`.
 
    Additional clauses:
@@ -308,6 +307,13 @@ described elsewhere
 
          Search is:Instance [ Reflexive | Symmetric ].
 
+      The following search outputs operations on `nat` defined in the
+      prelude either with the `Definition` or `Fixpoint` keyword:
+
+      .. coqtop:: all reset
+
+         Search (nat -> nat -> nat) -bool [ is:Definition | is:Fixpoint ].
+
 .. cmd:: SearchPattern @one_pattern {? {| inside | in | outside } {+ @qualid } }
 
    Displays the name and type of all hypotheses of the

diff --git 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" ]
+| [ "Fixpoint" | "CoFixpoint" | "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
 | [ "Field" | "Method" ]
 ]