1 files changed, 0 insertions, 100 deletions
diff --git a/theories7/Sets/Partial_Order.v b/theories7/Sets/Partial_Order.v
deleted file mode 100755
index 759cf4e2..00000000
--- a/theories7/Sets/Partial_Order.v
+++ /dev/null
@@ -1,100 +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        *)
-(************************************************************************)
-(****************************************************************************)
-(*                                                                          *)
-(*                         Naive Set Theory in Coq                          *)
-(*                                                                          *)
-(*                     INRIA                        INRIA                   *)
-(*              Rocquencourt                        Sophia-Antipolis        *)
-(*                                                                          *)
-(*                                 Coq V6.1                                 *)
-(*									    *)
-(*			         Gilles Kahn 				    *)
-(*				 Gerard Huet				    *)
-(*									    *)
-(*									    *)
-(*                                                                          *)
-(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
-(* to the Newton Institute for providing an exceptional work environment    *)
-(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
-(****************************************************************************)
-
-(*i $Id: Partial_Order.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*)
-
-Require Export Ensembles.
-Require Export Relations_1.
-
-Section Partial_orders.
-Variable U: Type.
-
-Definition Carrier :=  (Ensemble U).
-
-Definition Rel :=  (Relation U).
-
-Record PO : Type := Definition_of_PO {
-   Carrier_of: (Ensemble U);
-   Rel_of: (Relation U);
-   PO_cond1: (Inhabited U Carrier_of);
-   PO_cond2: (Order U Rel_of) }.
-Variable p: PO.
-
-Definition Strict_Rel_of : Rel :=  [x, y: U] (Rel_of p x y) /\ ~ x == y.
-
-Inductive covers [y, x:U]: Prop :=
-      Definition_of_covers:
-      (Strict_Rel_of x y) -> 
-          ~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) -> 
-          (covers y x).
-
-End Partial_orders.
-
-Hints Unfold Carrier_of Rel_of  Strict_Rel_of : sets v62.
-Hints Resolve Definition_of_covers : sets v62.
-
-
-Section Partial_order_facts.
-Variable U:Type.
-Variable D:(PO U).
-
-Lemma Strict_Rel_Transitive_with_Rel:
-  (x:U) (y:U) (z:U) (Strict_Rel_of U D x y) -> (Rel_of U D y z) ->
-  (Strict_Rel_of U D x z).
-Unfold 1 Strict_Rel_of.
-Red.
-Elim D; Simpl.
-Intros C R H' H'0; Elim H'0.
-Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
-Apply H'2 with y := y; Tauto.
-Red; Intro H'6.
-Elim H'4; Intros H'7 H'8; Apply H'8; Clear H'4.
-Apply H'3; Auto.
-Rewrite H'6; Tauto.
-Qed.
-
-Lemma Strict_Rel_Transitive_with_Rel_left:
-  (x:U) (y:U) (z:U) (Rel_of U D x y) -> (Strict_Rel_of U D y z) ->
-  (Strict_Rel_of U D x z).
-Unfold 1 Strict_Rel_of.
-Red.
-Elim D; Simpl.
-Intros C R H' H'0; Elim H'0.
-Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
-Apply H'2 with y := y; Tauto.
-Red; Intro H'6.
-Elim H'5; Intros H'7 H'8; Apply H'8; Clear H'5.
-Apply H'3; Auto.
-Rewrite <- H'6; Auto.
-Qed.
-
-Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)).
-Red.
-Intros x y z H' H'0.
-Apply Strict_Rel_Transitive_with_Rel with y := y; 
-  [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ].
-Qed.
-End Partial_order_facts.