aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-24 17:15:11 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-24 17:15:11 +0000
commitf7dbf2c0cb26fffb6bb13aeb1a76479569896c76 (patch)
tree4ddfa697d86d4b7e9b93154b3bd789ecbbb29ec0 /doc
parent094ccb1e4a9bf7af9e299f93a4346e388f22e9e2 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8451 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/Translator.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Translator.tex b/doc/Translator.tex
index fb2effc01..5ebee7fdf 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -526,7 +526,7 @@ arises:
\TRANS{true_sub}{Pminus}
\TRANS{entier}{N}
\TRANS{Un_suivi_de}{Ndouble_plus_one}
-\TRANS{Zero_suivi_de}{Ndouble
+\TRANS{Zero_suivi_de}{Ndouble}
\TRANS{Nul}{N0}
\TRANS{Pos}{Npos}
\end{transbox}