aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-17 19:56:25 +0000
committerGravatar emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-17 19:56:25 +0000
commitd5d1435708577eab01d711e4924ad2113660aba8 (patch)
tree36769155ec700bc1e86e39940d1c921f5ce40502 /doc
parentcc65a9b7754e9645ac72e629ce0b31359d8814cc (diff)
Corrected a LaTeX typo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-lib.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 3d22663c6..f1913d7cc 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -329,7 +329,6 @@ them come with a special syntax shown on Figure~\ref{specif-syntax}.
\subsubsection[Programming]{Programming\label{Programming}
\index{Programming}
\label{libnats}
-
\ttindex{unit}
\ttindex{tt}
\ttindex{bool}