From 41beba06c59bd5c4e954b46f27c7667be58f4982 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 14 Jan 2010 14:18:31 +0000
Subject: Avoid some more re-declarations of Equivalence instances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZOrder.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/NatInt')

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index ed59bca436..aa41a35ea9 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -127,7 +127,7 @@ Module OrderElts <: TotalOrder.
  Definition eq := eq.
  Definition lt := lt.
  Definition le := le.
- Instance eq_equiv : Equivalence eq.
+ Definition eq_equiv := eq_equiv.
  Instance lt_strorder : StrictOrder lt.
  Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-- 
cgit v1.2.3