Documenting the changes of Locate semantics.

1 files changed, 16 insertions, 2 deletions

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