diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-14 15:01:00 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-14 15:01:00 +0000 |
commit | f548bcddd7aca88889978c092747e4427017cd43 (patch) | |
tree | 8dbfc2f39774a0dbfd49b9ad1e978a632f1391c1 /doc/stdlib | |
parent | f31923c002943eebd7601871658cd636f7f2de4e (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-x | doc/stdlib/Library.tex | 37 |
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 |