From cae09e5af6cf31d96662b1b66a63c6a236a8e741 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin 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') 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