From 3b5e12a2eb98b34cacc1850f63b702dfea26cd57 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Feb 2010 20:24:10 +0000
Subject: Cleanup in Classes, removing unsupported code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12748 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/Functions.v    | 43 -----------------------------------------
 theories/Classes/SetoidAxioms.v | 36 ----------------------------------
 theories/Classes/SetoidClass.v  |  1 -
 theories/Classes/vo.itarget     |  2 --
 4 files changed, 82 deletions(-)
 delete mode 100644 theories/Classes/Functions.v
 delete mode 100644 theories/Classes/SetoidAxioms.v

diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
deleted file mode 100644
index 5efa4fa8f5..0000000000
--- a/theories/Classes/Functions.v
+++ /dev/null
@@ -1,43 +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        *)
-(************************************************************************)
-
-(** * Functional morphisms.
-
-   Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - University Paris Sud
-*)
-
-(* $Id$ *)
-
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
-
-Generalizable Variables A B eqA eqB RA RB f.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Class Injective `(m : Proper (A -> B) (RA ++> RB) f) : Prop :=
-  injective : forall x y : A, RB (f x) (f y) -> RA x y.
-
-Class Surjective `(m : Proper (A -> B) (RA ++> RB) f) : Prop :=
-  surjective : forall y, exists x : A, RB y (f x).
-
-Definition Bijective `(m : Proper (A -> B) (RA ++> RB) (f : A -> B)) :=
-  Injective m /\ Surjective m.
-
-Class MonoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) :=
-  monic :> Injective m.
-
-Class EpiMorphism `(m : Proper (A -> B) (eqA ++> eqB)) :=
-  epic :> Surjective m.
-
-Class IsoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) :=
-  { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }.
-
-Class AutoMorphism `(m : Proper (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
deleted file mode 100644
index 3789bb66f9..0000000000
--- a/theories/Classes/SetoidAxioms.v
+++ /dev/null
@@ -1,36 +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        *)
-(************************************************************************)
-
-(** * Extensionality axioms that can be used when reasoning with setoids.
-
-   Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - University Paris Sud
-*)
-
-(* $Id$ *)
-
-Require Import Coq.Program.Program.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Generalizable Variables a.
-
-Require Export Coq.Classes.SetoidClass.
-
-(** Application of the extensionality axiom to turn a goal on
-   Leibniz equality to a setoid equivalence (use with care!). *)
-
-Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
-
-(** Application of the extensionality principle for setoids. *)
-
-Ltac setoid_extensionality :=
-  match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index df1c0f7579..c41c576982 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -24,7 +24,6 @@ Require Import Coq.Program.Program.
 Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
-Require Import Coq.Classes.Functions.
 
 (** A setoid wraps an equivalence. *)
 
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
index fcd3a77df9..9daf133b44 100644
--- a/theories/Classes/vo.itarget
+++ b/theories/Classes/vo.itarget
@@ -1,12 +1,10 @@
 Equivalence.vo
 EquivDec.vo
-Functions.vo
 Init.vo
 Morphisms_Prop.vo
 Morphisms_Relations.vo
 Morphisms.vo
 RelationClasses.vo
-SetoidAxioms.vo
 SetoidClass.vo
 SetoidDec.vo
 SetoidTactics.vo
-- 
cgit v1.2.3