aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Correctness.tex
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-17 12:39:08 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-10-17 12:39:08 +0000
commit79757247806cffb089fab51ad6256d9e5142bbc2 (patch)
treee0925f711fafacc5f1be154c28975eb42727e123 /doc/Correctness.tex
parent4fe518a1c458d7d6274ac1c1b2f97504e1652f56 (diff)
Corrections diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Correctness.tex')
-rw-r--r--doc/Correctness.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Correctness.tex b/doc/Correctness.tex
index 6021ec9a7..7c8d97fc5 100644
--- a/doc/Correctness.tex
+++ b/doc/Correctness.tex
@@ -659,7 +659,7 @@ following:
\texttt{Exchange}).
\item[Sorted]: this module defines the property for an array to be
- sorted, on the whole array (\texttt{sorted\_array}) or on a segment
+ sorted, either on the whole array (\texttt{sorted\_array}) or on a segment
(\texttt{sub\_sorted\_array}). It also provides a few lemmas to
establish this property.
\end{description}