From f095df8c523d859fb4624631ec940eef89bfd8dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Apr 2010 09:08:13 +0000
Subject: Documenting the use of ##, %%, $$ in coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12909 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/coqdoc.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index e00484e6c1..271a13f7f6 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -167,6 +167,8 @@ escape sequences:
   discarded in \LaTeX\ output.
 \end{itemize}
 
+Note: to simply output the characters \verb+$+, \verb+%+ and \verb+#+
+and escaping their escaping role, these characters must be doubled.
 
 \paragraph{Verbatim.} 
 Verbatim material is introduced by a leading \verb+<<+ and closed by
-- 
cgit v1.2.3