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, 30 insertions, 35 deletions

diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 32f433d07..06440fd86 100755
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -10,19 +10,19 @@
 
 Section Relation_Definition.
 
-   Variable A: Type.
+   Variable A : Type.
    
-   Definition relation :=  A -> A -> Prop.
+   Definition relation := A -> A -> Prop.
 
-   Variable R: relation.
+   Variable R : relation.
    
 
 Section General_Properties_of_Relations.
 
-  Definition reflexive : Prop :=  (x: A) (R x x).
-  Definition transitive : Prop :=  (x,y,z: A) (R x y) -> (R y z) -> (R x z).
-  Definition symmetric : Prop :=  (x,y: A) (R x y) -> (R y x).
-  Definition antisymmetric : Prop :=  (x,y: A) (R x y) -> (R y x) -> x=y.
+  Definition reflexive : Prop := forall x:A, R x x.
+  Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
+  Definition symmetric : Prop := forall x y:A, R x y -> R y x.
+  Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y.
 
   (* for compatibility with Equivalence in  ../PROGRAMS/ALG/  *)
   Definition equiv := reflexive /\ transitive /\ symmetric.
@@ -33,23 +33,20 @@ End General_Properties_of_Relations.
 
 Section Sets_of_Relations.
 
-   Record preorder : Prop := {
-       preord_refl  : reflexive;
-       preord_trans : transitive }.
+   Record preorder : Prop := 
+     {preord_refl : reflexive; preord_trans : transitive}.
 
-   Record order : Prop := {
-       ord_refl    : reflexive;
-       ord_trans   : transitive;
-       ord_antisym : antisymmetric }.
+   Record order : Prop := 
+     {ord_refl : reflexive;
+      ord_trans : transitive;
+      ord_antisym : antisymmetric}.
 
-   Record equivalence : Prop := {
-       equiv_refl  : reflexive;
-       equiv_trans : transitive;
-       equiv_sym   : symmetric }.
+   Record equivalence : Prop := 
+     {equiv_refl : reflexive;
+      equiv_trans : transitive;
+      equiv_sym : symmetric}.
    
-   Record PER : Prop := {
-       per_sym   : symmetric;
-       per_trans : transitive }.
+   Record PER : Prop :=  {per_sym : symmetric; per_trans : transitive}.
 
 End Sets_of_Relations.
 
@@ -57,27 +54,25 @@ End Sets_of_Relations.
 
 Section Relations_of_Relations.
 
-  Definition inclusion : relation -> relation -> Prop :=
-      [R1,R2: relation] (x,y:A) (R1 x y) -> (R2 x y).
+  Definition inclusion (R1 R2:relation) : Prop :=
+    forall x y:A, R1 x y -> R2 x y.
 
-  Definition same_relation : relation -> relation -> Prop :=
-      [R1,R2: relation] (inclusion R1 R2) /\ (inclusion R2 R1).
+  Definition same_relation (R1 R2:relation) : Prop :=
+    inclusion R1 R2 /\ inclusion R2 R1.
    
-  Definition commut : relation -> relation -> Prop :=
-      [R1,R2:relation] (x,y:A) (R1 y x) -> (z:A) (R2 z y)
-                          -> (EX y':A |(R2 y' x) & (R1 z y')).
+  Definition commut (R1 R2:relation) : Prop :=
+    forall x y:A,
+      R1 y x -> forall z:A, R2 z y ->  exists2 y' : A | R2 y' x & R1 z y'.
 
 End Relations_of_Relations.
 
    
 End Relation_Definition.
 
-Hints Unfold reflexive transitive antisymmetric symmetric : sets v62.
+Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
 
-Hints Resolve Build_preorder Build_order Build_equivalence 
-	Build_PER preord_refl preord_trans 
-	ord_refl ord_trans ord_antisym
-	equiv_refl equiv_trans equiv_sym
-	per_sym per_trans : sets v62.
+Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
+  preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
+  equiv_trans equiv_sym per_sym per_trans: sets v62.
 
-Hints Unfold inclusion same_relation commut : sets v62.
+Hint Unfold inclusion same_relation commut: sets v62.
\ No newline at end of file