Update refman's Search documentation

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -188,17 +188,17 @@ described elsewhere
       .. insertprodn logical_kind logical_kind
 
       .. prodn::
-         logical_kind ::= Fixpoint
-         | CoFixpoint
+         logical_kind ::=
          | {| @thm_token | @assumption_token }
+         | {| Fixpoint | CoFixpoint }
          | {| Definition | Example | Context | Primitive | Symbol }
          | {| 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
+      `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>`.
 
@@ -308,6 +308,17 @@ described elsewhere
 
          Search is:Instance [ Reflexive | Symmetric ].
 
+      The following search outputs operations on `nat` defined either with
+      the `Definition` or `Fixpoint`
+
+      .. coqtop:: none reset
+
+         Require Import PeanoNat.
+
+      .. coqtop:: all
+
+         Search (nat -> nat -> nat) [ is:Definition | is:Fixpoint ].
+
 .. cmd:: SearchPattern @one_pattern {? {| inside | in | outside } {+ @qualid } }
 
    Displays the name and type of all hypotheses of the