Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 13 insertions, 13 deletions

diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 64c4c654..85d0cffc 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -24,42 +24,42 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Section Relations_1.
    Variable U : Type.
-   
+
    Definition Relation := U -> U -> Prop.
    Variable R : Relation.
-   
+
    Definition Reflexive : Prop := forall x:U, R x x.
-   
+
    Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z.
-   
+
    Definition Symmetric : Prop := forall x y:U, R x y -> R y x.
-   
+
    Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y.
-   
+
    Definition contains (R R':Relation) : Prop :=
      forall x y:U, R' x y -> R x y.
-   
+
    Definition same_relation (R R':Relation) : Prop :=
      contains R R' /\ contains R' R.
-   
+
    Inductive Preorder : Prop :=
        Definition_of_preorder : Reflexive -> Transitive -> Preorder.
-   
+
    Inductive Order : Prop :=
        Definition_of_order :
          Reflexive -> Transitive -> Antisymmetric -> Order.
-   
+
    Inductive Equivalence : Prop :=
        Definition_of_equivalence :
          Reflexive -> Transitive -> Symmetric -> Equivalence.
-   
+
    Inductive PER : Prop :=
        Definition_of_PER : Symmetric -> Transitive -> PER.
-   
+
 End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets v62.