Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 9 insertions, 9 deletions

diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index b8c65148..970db182 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_2.
@@ -32,26 +32,26 @@ Require Export Relations_2.
 Section Relations_3.
    Variable U : Type.
    Variable R : Relation U.
-   
+
    Definition coherent (x y:U) : Prop :=
       exists z : _, Rstar U R x z /\ Rstar U R y z.
-   
+
    Definition locally_confluent (x:U) : Prop :=
      forall y z:U, R x y -> R x z -> coherent y z.
-   
+
    Definition Locally_confluent : Prop := forall x:U, locally_confluent x.
-   
+
    Definition confluent (x:U) : Prop :=
      forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.
-   
+
    Definition Confluent : Prop := forall x:U, confluent x.
-   
+
    Inductive noetherian (x: U) : Prop :=
        definition_of_noetherian :
          (forall y:U, R x y -> noetherian y) -> noetherian x.
-   
+
    Definition Noetherian : Prop := forall x:U, noetherian x.
-   
+
 End Relations_3.
 Hint Unfold coherent: sets v62.
 Hint Unfold locally_confluent: sets v62.