From 104df916312521ea5a8a5d7293ca539beef768ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Mar 2015 15:44:49 +0100
Subject: Fixing #4127 (command for locating exists notation in refman
 changed).

---
 doc/refman/RefMan-syn.tex | 6 ++++--
 1 file 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}
-- 
cgit v1.2.3