Documenting the changes of Locate semantics.

2 files changed, 19 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index f5e83bdaed..5d904f305d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,9 @@ Vernacular commands
   The tools/update-require script can be used to convert a development.
 - A new Print Strategies command allows to visualize the opacity status
   of the whole engine.
+- The "Locate" command now searches through all sorts of qualified namespaces of
+  Coq: terms, modules, tactics, etc. The old behaviour of the command can be
+  retrieved using the "Locate Term" command.
 
 Specification Language
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 20ead7cceb..8aa6df0616 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -421,8 +421,10 @@ The default blacklisted substrings are {\tt "\_admitted"
 
 \subsection[\tt Locate {\qualid}.]{\tt Locate {\qualid}.\comindex{Locate}
 \label{Locate}}
-This command displays the full name of the qualified identifier {\qualid}
-and consequently the \Coq\ module in which it is defined.
+This command displays the full name of objects whose name is a prefix of the
+qualified identifier {\qualid}, and consequently the \Coq\ module in which they
+are defined. It searches for objects from the different qualified namespaces of
+Coq: terms, modules, Ltac, etc.
 
 \begin{coq_eval}
 (*************** The last line should produce **************************)
@@ -439,6 +441,18 @@ Locate Coq.Init.Datatypes.O.
 Locate I.Dont.Exist.
 \end{coq_example}
 
+\begin{Variants}
+\item {\tt Locate Term {\qualid}.}\comindex{Locate Term}\\
+  As {\tt Locate} but restricted to terms.
+
+\item {\tt Locate Module {\qualid}.}
+  As {\tt Locate} but restricted to modules.
+
+\item {\tt Locate Ltac {\qualid}.}\comindex{Locate Ltac}\\
+  As {\tt Locate} but restricted to tactics.
+\end{Variants}
+
+
 \SeeAlso Section \ref{LocateSymbol}
 
 \subsection{The {\sc Whelp} searching tool