Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 51 insertions, 51 deletions

diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index f3d692b85..5ef6bc9b0 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -30,71 +30,71 @@ Require Export Ensembles.
 Require Export Relations_1.
 
 Section Partial_orders.
-Variable U: Type.
+Variable U : Type.
 
-Definition Carrier :=  (Ensemble U).
+Definition Carrier := Ensemble U.
 
-Definition Rel :=  (Relation 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.
+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.
+Definition Strict_Rel_of : Rel := fun 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).
+Inductive covers (y x:U) : Prop :=
+    Definition_of_covers :
+      Strict_Rel_of x y ->
+      ~ ( exists 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.
+Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62.
+Hint Resolve Definition_of_covers: sets v62.
 
 
 Section Partial_order_facts.
-Variable U:Type.
-Variable D:(PO U).
+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.
+Lemma Strict_Rel_Transitive_with_Rel :
+ forall x y z:U,
+   Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+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 in |- *; 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.
+Lemma Strict_Rel_Transitive_with_Rel_left :
+ forall x y z:U,
+   Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+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 in |- *; 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 ].
+Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
+red in |- *.
+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.
+End Partial_order_facts.
\ No newline at end of file