23 files changed, 0 insertions, 184 deletions
diff --git a/README.doc b/README.doc
index 4e72c894b..4e72c894b 100755..100644
--- a/README.doc
+++ b/README.doc
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 0e820008e..0e820008e 100755..100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156..4716c3156 100755..100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index 44a0b1d36..44a0b1d36 100755..100644
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 836944ab1..836944ab1 100755..100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index 0d75d52a3..0d75d52a3 100755..100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 0d75d52a3..0d75d52a3 100755..100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
deleted file mode 100755
index 655de34ca..000000000
--- a/theories/Arith/intro.tex
+++ /dev/null
@@ -1,55 +0,0 @@
-\section{Arith}\label{Arith}
-
-The {\tt Arith} library deals with various arithmetical notions and 
-their properties.
-
-\subsection*{Standard {\tt Arith} library}
-
-The following files are automatically loaded by {\tt Require Arith}.
-
-\begin{itemize}
-
-\item {\tt Le.v} states and proves properties of the large order {\tt le}.
-
-\item {\tt Lt.v} states and proves properties of the strict order {\tt 
-lt} (especially, the relationship with {\tt le}).
-
-\item {\tt Plus.v} states and proves properties on the addition.
-
-\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}.
-
-\item {\tt Minus.v} defines the difference on 
-{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is 
-{\tt O} if {\tt n} $<$ {\tt p}.
-
-\item {\tt Mult.v} states and proves properties on the multiplication.
-
-\item {\tt Between.v} defines modalities on {\tt nat} and proves properties 
-of them.
-
-\end{itemize}
-
-\subsection*{Additional {\tt Arith} library}
-
-\begin{itemize}
-
-\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state
-and prove various decidability results on {\tt nat}.
-
-\item {\tt Wf\_nat.v} states and proves various induction and recursion 
-principles on {\tt nat}. Especially, recursion for objects measurable by 
-a natural number and recursion on {\tt nat * nat} are provided.
-
-\item {\tt Min.v} defines the minimum of two natural numbers and proves 
-properties of it. 
-
-\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
-the equivalence with Leibniz' equality.
-
-\item {\tt Euclid.v} proves that the euclidean
-division specification is realisable. Conversely, {\tt Div.v} exhibits
-two different algorithms and semi-automatically reconstruct the proof of
-their correctness. These files emphasize the extraction of program vs
-reconstruction of proofs paradigm.
-
-\end{itemize}
diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex
deleted file mode 100644
index 22ee38aab..000000000
--- a/theories/Bool/intro.tex
+++ /dev/null
@@ -1,16 +0,0 @@
-\section{Bool}\label{Bool}
-
-The BOOL library includes the following files:
-
-\begin{itemize}
-
-\item {\tt Bool.v} defines standard operations on booleans and states
-  and proves simple facts on them.
-\item {\tt IfProp.v} defines a disjunction which contains its proof
-  and states its properties.
-\item {\tt Zerob.v} defines the test against 0 on natural numbers and
-  states and proves properties of it.
-\item {\tt Orb.v} states and proves facts on the boolean or.
-\item {\tt DecBool.v} defines a conditional from a proof of
-  decidability and states its properties.
-\end{itemize}
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
deleted file mode 100755
index d372de8ed..000000000
--- a/theories/Lists/intro.tex
+++ /dev/null
@@ -1,20 +0,0 @@
-\section{Lists}\label{Lists}
-
-This library includes the following files:
-
-\begin{itemize}
-
-\item {\tt List.v} contains definitions of (polymorphic) lists, 
-  functions on lists such as head, tail, map, append and prove some
-  properties of these functions. Implicit arguments are used in this
-  library, so you should read the Reference Manual about implicit
-  arguments before using it.
-
-\item {\tt ListSet.v} contains definitions and properties of finite
-  sets, implemented as lists.
-
-\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
-  co-inductive type. Basic facts are stated and proved. The streams are
-  also polymorphic.
-
-\end{itemize}
diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex
deleted file mode 100755
index 1fb294f2f..000000000
--- a/theories/Logic/intro.tex
+++ /dev/null
@@ -1,8 +0,0 @@
-\section{Logic}\label{Logic}
-
-This library deals with classical logic and its properties.
-The main file is {\tt Classical.v}.
-
-This library also provides some facts on equalities for dependent
-types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.
-
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
deleted file mode 100644
index bf39bc36c..000000000
--- a/theories/NArith/intro.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-\section{Binary natural numbers : NArith}\label{NArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex
deleted file mode 100644
index ffce881ed..000000000
--- a/theories/PArith/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Binary positive integers : PArith}\label{PArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex
deleted file mode 100644
index 433172585..000000000
--- a/theories/Reals/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Reals}\label{Reals}
-
-This library contains an axiomatization of real numbers.
-The main file is \texttt{Reals.v}.
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
deleted file mode 100755
index 5056f36f9..000000000
--- a/theories/Relations/intro.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{Relations}\label{Relations}
-
-This library develops closure properties of relations.
-
-\begin{itemize}
-\item {\tt Relation\_Definitions.v} deals with the general notions
-  about binary relations (orders, equivalences, ...)
-
-\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
-  closures of relations (by symmetry, by transitivity, ...) and
-  lexicographic orderings.
-
-\item {\tt Operators\_Properties.v} states and proves facts on the
-  various closures of a relation.
-
-\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
-    Relation\_Operators.v} and \\
-    {\tt Operators\_Properties.v} together.
-
-\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
-  confluent relations.
-
-\end{itemize}
diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex
deleted file mode 100644
index 50cd025de..000000000
--- a/theories/Setoids/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Setoids}\label{Setoids}
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
deleted file mode 100755
index 83c2177fd..000000000
--- a/theories/Sets/intro.tex
+++ /dev/null
@@ -1,24 +0,0 @@
-\section{Sets}\label{Sets}
-
-This is a library on sets defined by their characteristic predicate.
-It contains the following modules:
-
-\begin{itemize}
-\item {\tt Ensembles.v}
-\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
-\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, 
- {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v},  \\
- {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
-\item {\tt Partial\_Order.v}, {\tt Cpo.v}
-\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, 
- {\tt Powerset\_Classical\_facts.v}
-\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
-\item {\tt Image.v}
-\item {\tt Infinite\_sets.v}
-\item {\tt Integers.v}
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex
deleted file mode 100644
index 64ae4c888..000000000
--- a/theories/Sorting/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Sorting}\label{Sorting}
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
deleted file mode 100755
index 126071e28..000000000
--- a/theories/Wellfounded/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Well-founded relations}\label{Wellfounded}
-
-This library gives definitions and results about well-founded relations.
-
diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex
deleted file mode 100755
index 21e52c198..000000000
--- a/theories/ZArith/intro.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-\section{Binary integers : ZArith}
-The {\tt ZArith} library deals with binary integers (those used
-by the {\tt Omega} decision tactic).
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/tools/README.coq-tex b/tools/README.coq-tex
deleted file mode 100755
index 5c7606a96..000000000
--- a/tools/README.coq-tex
+++ /dev/null
@@ -1,13 +0,0 @@
-DESCRIPTION.
-
-The coq-tex filter extracts Coq phrases embedded in LaTeX files,
-evaluates them, and insert the outcome of the evaluation after each
-phrase.
-
-The filter is written in Perl, so you'll need Perl version 4 installed
-on your machine.
-
-USAGE. See the manual page (coq-tex.1).
-
-AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr)
-  from caml-tex of Xavier Leroy.
diff --git a/tools/README.emacs b/tools/README.emacs
index 4d8e3697a..4d8e3697a 100755..100644
--- a/tools/README.emacs
+++ b/tools/README.emacs
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
index 9f6e5480c..9f6e5480c 100755..100644
--- a/tools/coq-sl.sty
+++ b/tools/coq-sl.sty