diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 18 |
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 |