From 35c834548dcbd590f66f009017d2f88797dce882 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 26 Jun 2014 16:37:05 +0200
Subject: Remove some theories that have been deprecated for 10 years.

---
 theories/Logic/Classical_Pred_Set.v      | 48 --------------------------------
 theories/Logic/Classical_Type.v          | 14 ----------
 theories/Logic/vo.itarget                |  2 --
 theories/Sets/Classical_sets.v           |  2 +-
 theories/Sets/Finite_sets_facts.v        |  2 +-
 theories/Sets/Image.v                    |  2 +-
 theories/Sets/Infinite_sets.v            |  2 +-
 theories/Sets/Integers.v                 |  2 +-
 theories/Sets/Powerset_Classical_facts.v |  2 +-
 9 files changed, 6 insertions(+), 70 deletions(-)
 delete mode 100644 theories/Logic/Classical_Pred_Set.v
 delete mode 100644 theories/Logic/Classical_Type.v

diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
deleted file mode 100644
index cda9d22c6c..0000000000
--- a/theories/Logic/Classical_Pred_Set.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* File created for Coq V5.10.14b, Oct 1995, by duplication of
-   Classical_Pred_Type.v *)
-
-(** This file is obsolete, use Classical_Pred_Type.v via Classical.v
-instead *)
-
-(** Classical Predicate Logic on Set*)
-
-Require Import Classical_Pred_Type.
-
-Section Generic.
-Variable U : Set.
-
-(** de Morgan laws for quantifiers *)
-
-Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
-Proof (Classical_Pred_Type.not_all_ex_not U).
-
-Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
-Proof (Classical_Pred_Type.not_all_not_ex U).
-
-Lemma not_ex_all_not :
- forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof (Classical_Pred_Type.not_ex_all_not U).
-
-Lemma not_ex_not_all :
- forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
-Proof (Classical_Pred_Type.not_ex_not_all U).
-
-Lemma ex_not_not_all :
- forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof (Classical_Pred_Type.ex_not_not_all U).
-
-Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
-Proof (Classical_Pred_Type.all_not_not_ex U).
-
-End Generic.
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
deleted file mode 100644
index 86fdd69f3e..0000000000
--- a/theories/Logic/Classical_Type.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file is obsolete, use Classical.v instead *)
-
-(** Classical Logic for Type *)
-
-Require Export Classical_Prop.
-Require Export Classical_Pred_Type.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index e703f2828e..488fd908ee 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -4,10 +4,8 @@ ClassicalChoice.vo
 ClassicalDescription.vo
 ClassicalEpsilon.vo
 ClassicalFacts.vo
-Classical_Pred_Set.vo
 Classical_Pred_Type.vo
 Classical_Prop.vo
-Classical_Type.vo
 ClassicalUniqueChoice.vo
 Classical.vo
 ConstructiveEpsilon.vo
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 3129dbb1e6..734564bed8 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -26,7 +26,7 @@
 
 Require Export Ensembles.
 Require Export Constructive_sets.
-Require Export Classical_Type.
+Require Export Classical.
 
 Section Ensembles_classical.
   Variable U : Type.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index c0613637e9..d6447d6235 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -26,7 +26,7 @@
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
-Require Export Classical_Type.
+Require Export Classical.
 Require Export Classical_sets.
 Require Export Powerset.
 Require Export Powerset_facts.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index bdb7c07751..701c95a876 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -26,7 +26,7 @@
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
-Require Export Classical_Type.
+Require Export Classical.
 Require Export Classical_sets.
 Require Export Powerset.
 Require Export Powerset_facts.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index 897046ab27..7031d5ddde 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -26,7 +26,7 @@
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
-Require Export Classical_Type.
+Require Export Classical.
 Require Export Classical_sets.
 Require Export Powerset.
 Require Export Powerset_facts.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 4ee7496e66..350a63f188 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -26,7 +26,7 @@
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
-Require Export Classical_Type.
+Require Export Classical.
 Require Export Classical_sets.
 Require Export Powerset.
 Require Export Powerset_facts.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index d24e931d5b..de12eaf8e1 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -32,7 +32,7 @@ Require Export Partial_Order.
 Require Export Cpo.
 Require Export Powerset.
 Require Export Powerset_facts.
-Require Export Classical_Type.
+Require Export Classical.
 Require Export Classical_sets.
 
 Section Sets_as_an_algebra.
-- 
cgit v1.2.3