diff options
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 6 |
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} |