diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 63b4a874a8f1e..12c2ce92fb18d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -198,7 +198,7 @@ described elsewhere
       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,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