aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2002-08-14 18:59:05 +0000
committerherbelin2002-08-14 18:59:05 +0000
commit1cca95b23a15ad0dfa3a79ff07ac57f870c333f0 (patch)
tree886ff42823706cd03463cde042845014201bbe7b
parent948ac45372c7ba99849eadb01ae8a1de1706eedd (diff)
Retour de Sorting dans la biblio standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8288 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xdoc/RefMan-lib.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 9677d3b5fd..b7e2628b60 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -814,6 +814,7 @@ subdirectories:
series, power series and results,... Requires the
\textbf{ZArith} library).\\
{\bf Relations} & Relations (definitions and basic results). \\
+ {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
{\bf Wellfounded} & Well-founded relations (basic results). \\
\end{tabular}