Imported Upstream version 8.5~beta3+dfsg

2 files changed, 10 insertions, 30 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index ea07a849..fe18686e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -45,8 +45,8 @@ Section Lists.
 
   Definition hd_error (l:list A) :=
     match l with
-      | [] => error
-      | x :: _ => value x
+      | [] => None
+      | x :: _ => Some x
     end.
 
   Definition tl (l:list A) :=
@@ -69,7 +69,7 @@ Section Facts.
   Variable A : Type.
 
 
-  (** *** Genereric facts *)
+  (** *** Generic facts *)
 
   (** Discrimination *)
   Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.
@@ -393,11 +393,11 @@ Section Elts.
     simpl; auto.
   Qed.
 
-  Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
+  Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A :=
     match n, l with
-      | O, x :: _ => value x
+      | O, x :: _ => Some x
       | S n, _ :: l => nth_error l n
-      | _, _ => error
+      | _, _ => None
     end.
 
   Definition nth_default (default:A) (l:list A) (n:nat) : A :=
@@ -622,9 +622,9 @@ Section Elts.
   Qed.
 
 
-  (****************************************)
-  (** ** Counting occurences of a element *)
-  (****************************************)
+  (******************************************)
+  (** ** Counting occurrences of an element *)
+  (******************************************)
 
   Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
@@ -2202,7 +2202,7 @@ Section ForallPairs.
   Proof.
     induction 1.
     inversion 1.
-    simpl; destruct 1; destruct 1; repeat subst; auto.
+    simpl; destruct 1; destruct 1; subst; auto.
     right; left. apply -> Forall_forall; eauto.
     right; right. apply -> Forall_forall; eauto.
   Qed.
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
deleted file mode 100755
index d372de8e..00000000
--- 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}