Nettoyage de l'archive doc et restructuration avant intégration à l'archive

principale de Coq et publication des sources (HH)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 60 insertions, 0 deletions

diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
new file mode 100755
index 000000000..58b2dc6df
--- /dev/null
+++ b/doc/stdlib/Library.tex
@@ -0,0 +1,60 @@
+\documentclass[11pt]{article}
+
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage[noweb]{coqweb}
+
+\input{./title}
+\input{./macros}
+
+\begin{document}
+ 
+\coverpage{The standard library}%
+{\ }
+
+\tableofcontents
+
+\newpage
+\section*{The \Coq\ standard library}
+
+This document is a short description of the \Coq\ standard library.
+This library comes with the system as a complement of the core library
+(the {\bf Init} library ; see the Reference Manual for a description
+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
+                  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
+
+Each of these subdirectories contains a set of modules, whose
+specifications (\gallina{} files) have
+been roughly, and automatically, pasted in the following pages. There
+is also a version of this document in HTML format on the WWW, which
+you can access from the \Coq\ home page at
+\texttt{http://coq.inria.fr/library}.
+
+\input{library.coqweb.tex}
+
+\end{document}
+
+% $Id$