Remove useless MonoList.v

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

5 files changed, 1 insertions, 275 deletions

diff --git a/Makefile.common b/Makefile.common
index 7116af96e..3c56226ef 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -346,7 +346,7 @@ QARITHVO:=$(addprefix theories/QArith/, \
  Qabs.vo        Qround.vo )
 
 LISTSVO:=$(addprefix theories/Lists/, \
- MonoList.vo  	ListSet.vo   	Streams.vo 	StreamMemo.vo  \
+ ListSet.vo   	Streams.vo 	StreamMemo.vo  \
  TheoryList.vo	List.vo 	SetoidList.vo   ListTactics.vo )
 
 STRINGSVO:=$(addprefix theories/Strings/, \
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 6b35dfa99..048fd6067 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -343,7 +343,6 @@ through the <tt>Require Import</tt> command.</p>
   <dd> 
     theories/Lists/List.v
     theories/Lists/ListSet.v
-    theories/Lists/MonoList.v
     theories/Lists/SetoidList.v
     theories/Lists/Streams.v
     theories/Lists/StreamMemo.v
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v
deleted file mode 100644
index 5aaf0b209..000000000
--- a/theories/Lists/MonoList.v
+++ /dev/null
@@ -1,269 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
-
-Require Import Le.
-
-Parameter List_Dom : Set.
-Definition A := List_Dom.
-
-Inductive list : Set :=
-  | nil : list
-  | cons : A -> list -> list.
-
-Fixpoint app (l m:list) {struct l} : list :=
-  match l return list with
-  | nil => m
-  | cons a l1 => cons a (app l1 m)
-  end.
-
-
-Lemma app_nil_end : forall l:list, l = app l nil.
-Proof. 
-	intro l; elim l; simpl in |- *; auto.
-        simple induction 1; auto.
-Qed.
-Hint Resolve app_nil_end: list v62.
-
-Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
-Proof. 
-	intros l m n; elim l; simpl in |- *; auto with list.
-	simple induction 1; auto with list.
-Qed.
-Hint Resolve app_ass: list v62.
-
-Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
-Proof. 
-	auto with list.
-Qed.
-Hint Resolve ass_app: list v62.
-
-Definition tail (l:list) : list :=
-  match l return list with
-  | cons _ m => m
-  | _ => nil
-  end.
-                   
-
-Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
-  intros; discriminate.
-Qed.
-
-(****************************************)
-(* Length of lists                      *)
-(****************************************)
-
-Fixpoint length (l:list) : nat :=
-  match l return nat with
-  | cons _ m => S (length m)
-  | _ => 0
-  end.
-
-(******************************)
-(* Length order of lists      *)
-(******************************)
-
-Section length_order.
-Definition lel (l m:list) := length l <= length m.
-
-Hint Unfold lel: list.
-
-Variables a b : A.
-Variables l m n : list.
-
-Lemma lel_refl : lel l l.
-Proof. 
-	unfold lel in |- *; auto with list.
-Qed.
-
-Lemma lel_trans : lel l m -> lel m n -> lel l n.
-Proof. 
-	unfold lel in |- *; intros.
-        apply le_trans with (length m); auto with list.
-Qed.
-
-Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_cons : lel l m -> lel l (cons b m).
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
-Proof. 
-	intro l'; elim l'; auto with list arith.
-	intros a' y H H0.
-	(*  <list>nil=(cons a' y)
-	    ============================
-	      H0 : (lel (cons a' y) nil)
-	      H : (lel y nil)->(<list>nil=y)
-	      y : list
-	      a' : A
-	      l' : list *)
-	absurd (S (length y) <= 0); auto with list arith.
-Qed.
-End length_order.
-
-Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
-  v62.
-
-Fixpoint In (a:A) (l:list) {struct l} : Prop :=
-  match l with
-  | nil => False
-  | cons b m => b = a \/ In a m
-  end.
-
-Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
-Proof. 
-	simpl in |- *; auto with list.
-Qed.
-Hint Resolve in_eq: list v62.
-
-Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
-Proof. 
-	simpl in |- *; auto with list.
-Qed.
-Hint Resolve in_cons: list v62.
-
-Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
-Proof. 
-	intros l m a.
-	elim l; simpl in |- *; auto with list.
-	intros a0 y H H0.
-	(*  ((<A>a0=a)\/(In a y))\/(In a m)
-	    ============================
-	      H0 : (<A>a0=a)\/(In a (app y m))
-	      H : (In a (app y m))->((In a y)\/(In a m))
-	      y : list
-	      a0 : A
-	      a : A
-	      m : list
-	      l : list *)
-	elim H0; auto with list.
-	intro H1.
-	(*  ((<A>a0=a)\/(In a y))\/(In a m)
-	    ============================
-	      H1 : (In a (app y m)) *)
-	elim (H H1); auto with list.
-Qed.
-Hint Immediate in_app_or: list v62.
-
-Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
-Proof. 
-	intros l m a.
-	elim l; simpl in |- *; intro H.
-	(* 1 (In a m)
-	    ============================
-	      H : False\/(In a m)
-	      a : A
-	      m : list
-	      l : list *)
-	elim H; auto with list; intro H0.
-	(*  (In a m)
-	    ============================
-	      H0 : False *)
-	elim H0. (* subProof completed *)
-	intros y H0 H1.
-	(*  2 (<A>H=a)\/(In a (app y m))
-	    ============================
-	      H1 : ((<A>H=a)\/(In a y))\/(In a m)
-	      H0 : ((In a y)\/(In a m))->(In a (app y m))
-	      y : list *)
-	elim H1; auto 4 with list.
-	intro H2.
-	(*  (<A>H=a)\/(In a (app y m))
-	    ============================
-	      H2 : (<A>H=a)\/(In a y) *)
-	elim H2; auto with list.
-Qed.
-Hint Resolve in_or_app: list v62.
-
-Definition incl (l m:list) := forall a:A, In a l -> In a m.
-
-Hint Unfold incl: list v62.
-
-Lemma incl_refl : forall l:list, incl l l.
-Proof. 
-	auto with list.
-Qed.
-Hint Resolve incl_refl: list v62.
-
-Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_tl: list v62.
-
-Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
-Proof. 
-	auto with list.
-Qed.
-
-Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_appl: list v62.
-
-Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_appr: list v62.
-
-Lemma incl_cons :
- forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
-Proof. 
-	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
-	(*  (In a0 m)
-	    ============================
-	      H1 : (<A>a=a0)\/(In a0 l)
-	      a0 : A
-	      H0 : (a:A)(In a l)->(In a m)
-	      H : (In a m)
-	      m : list
-	      l : list
-	      a : A *)
-	elim H1.
-	(*  1 (<A>a=a0)->(In a0 m) *)
-	elim H1; auto with list; intro H2.
-	(*  (<A>a=a0)->(In a0 m)
-	    ============================
-	      H2 : <A>a=a0 *)
-	elim H2; auto with list. (* solves subgoal *)
-	(*  2 (In a0 l)->(In a0 m) *)
-	auto with list.
-Qed.
-Hint Resolve incl_cons: list v62.
-
-Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
-Proof. 
-	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
-	(*  (In a n)
-	    ============================
-	      H1 : (In a (app l m))
-	      a : A
-	      H0 : (a:A)(In a m)->(In a n)
-	      H : (a:A)(In a l)->(In a n)
-	      n : list
-	      m : list
-	      l : list *)
-	elim (in_app_or l m a); auto with list.
-Qed.
-Hint Resolve incl_app: list v62.
\ No newline at end of file
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index c45f88036..0051e2c2e 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -21,7 +21,4 @@ This library includes the following files:
   coinductive type. Basic facts are stated and proved. The streams are
   also polymorphic.
 
-\item {\tt MonoList.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
-  WITH OLDER VERSIONS OF COQ. THE USER SHOULD USE {\tt List.v} INSTEAD.
-
 \end{itemize}
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 7798ebebc..fc7a1eca3 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -78,7 +78,6 @@ Init/Wf.vo
 Lists/ListSet.vo
 Lists/ListTactics.vo
 Lists/List.vo
-Lists/MonoList.vo
 Lists/SetoidList.vo
 Lists/StreamMemo.vo
 Lists/Streams.vo