Fixing #4127 (command for locating exists notation in refman changed).

1 files changed, 4 insertions, 2 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 107b98f010..37cbd1eac1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -427,9 +427,11 @@ To know to which notations a given symbol belongs to, use the command
 \begin{quote}
 \tt Locate {\symbolentry}
 \end{quote}
-where symbol is any (composite) symbol surrounded by quotes. To locate
+where symbol is any (composite) symbol surrounded by double quotes. To locate
 a particular notation, use a string where the variables of the
-notation are replaced by ``\_''.
+notation are replaced by ``\_'' and where possible single quotes
+inserted around identifiers or tokens starting with a single quote are
+dropped.
 
 \Example
 \begin{coq_example}