changed deprecated setoid into relation

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

1 files changed, 9 insertions, 10 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 2c80aff40..16733c3b8 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -157,16 +157,15 @@ Qed.
 
 (** We now consider [Q] seen as a setoid. *)
 
-Definition Q_Setoid : Setoid_Theory Q Qeq.
-Proof.
- split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
-Qed.
-
-Add Setoid Q Qeq Q_Setoid as Qsetoid.
-
-Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
+Add Relation Q Qeq
+  reflexivity proved by Qeq_refl
+  symmetry proved by Qeq_sym
+  transitivity proved by Qeq_trans
+as Q_Setoid.
+
+Hint Resolve Qeq_refl : qarith.
+Hint Resolve Qeq_sym : qarith.
+Hint Resolve Qeq_trans : qarith.
 
 Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
 Proof.