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, 0 insertions, 60 deletions

diff --git a/doc/Library.tex b/doc/Library.tex
deleted file mode 100755
index 58b2dc6df9..0000000000
--- a/doc/Library.tex
+++ /dev/null
@@ -1,60 +0,0 @@
-\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$