From cae09e5af6cf31d96662b1b66a63c6a236a8e741 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 9 Mar 2017 15:36:42 +0100
Subject: Typo doc notations.

---
 doc/refman/RefMan-syn.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-syn.tex')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index b7d36ecaa..61093709e 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -303,7 +303,7 @@ the possible following elements delimited by single quotes:
   of each newline
 \end{itemize}
 
-Thus, for the previous example, we get
+%Thus, for the previous example, we get
 %\footnote{The ``@'' is here to shunt
 %the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq}
 %initial state}:
-- 
cgit v1.2.3

