aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-14 15:01:00 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-14 15:01:00 +0000
commitf548bcddd7aca88889978c092747e4427017cd43 (patch)
tree8dbfc2f39774a0dbfd49b9ad1e978a632f1391c1 /doc/stdlib
parentf31923c002943eebd7601871658cd636f7f2de4e (diff)
r8637@thot: notin | 2006-03-14 16:00:49 +0100
- intégration de doc dans le Makefile principal - correction d'une incompatibilité avec Tetex 3.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
-rwxr-xr-xdoc/stdlib/Library.tex37
1 files changed, 18 insertions, 19 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index edda403aa..ee14589cf 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -28,26 +28,25 @@ of this library). It provides a set of modules directly available
through the \verb!Require! command.
The standard library is composed of the following subdirectories:
-\medskip
-\begin{tabular}{lp{12cm}}
- {\bf Logic} & Classical logic and dependent equality \\
- {\bf Bool} & Booleans (basic functions and results) \\
- {\bf Arith} & Basic Peano arithmetic \\
- {\bf ZArith} & Basic integer arithmetic \\
- {\bf Reals} & Classical Real Numbers and Analysis \\
- {\bf Lists} & Monomorphic and polymorphic lists (basic functions and
+\begin{description}
+ \item[Logic] Classical logic and dependent equality
+ \item[Bool] Booleans (basic functions and results)
+ \item[Arith] Basic Peano arithmetic
+ \item[ZArith] Basic integer arithmetic
+ \item[Reals] Classical Real Numbers and Analysis
+ \item[Lists] Monomorphic and polymorphic lists (basic functions and
results), Streams (infinite sequences defined
- with co-inductive types) \\
- {\bf Sets} & Sets (classical, constructive, finite, infinite, power set,
- etc.) \\
- {\bf Relations} & Relations (definitions and basic results). \\
- {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
- {\bf Wellfounded} & Well-founded relations (basic results). \\
- {\bf IntMap} & Representation of finite sets by an efficient
- structure of map (trees indexed by binary integers).\\
-
-\end{tabular}
-\medskip
+ with co-inductive types)
+ \item[Sets] Sets (classical, constructive, finite, infinite, power set,
+ etc.)
+ \item[Relations] Relations (definitions and basic results).
+ \item[Sorting] Sorted list (basic definitions and heapsort
+ correctness).
+ \item[Wellfounded] Well-founded relations (basic results).
+ \item[IntMap] Representation of finite sets by an efficient
+ structure of map (trees indexed by binary integers).
+\end{description}
+
Each of these subdirectories contains a set of modules, whose
specifications (\gallina{} files) have