Merge PR #18074: Explain "Constant" in Locate output

Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
coq · May 22, 2024 · 1bae91e · 1bae91e
2 parents f1649da + 38d5aec
commit 1bae91e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -417,6 +417,10 @@ Requests to the environment
    are reported only when the containing module has been imported
    (e.g. with :cmd:`Require Import` or :cmd:`Import`).
 
+   Objects defined with commands such as :cmd:`Definition`, :cmd:`Parameter`,
+   :cmd:`Record`, :cmd:`Theorem` and their numerous variants are shown
+   as `Constant` in the output.
+
    :n:`@qualid`
      refers to object names that end with :n:`@qualid`.