diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-09 15:36:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-09 15:40:20 +0100 |
| commit | cae09e5af6cf31d96662b1b66a63c6a236a8e741 (patch) | |
| tree | b4d6de65e51a43033771aa68723a36c8b61f3380 /doc | |
| parent | b7415c84269b1553470216b06871def933e2f3bd (diff) | |
Typo doc notations.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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}: |