From bc1168a4aa0a336e9686b57cc29ec562aa379973 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Dec 2009 15:27:45 +0000
Subject: RelationPairs: stop loading it in all Numbers, stop maximal args with
 fst/snd

 As a consequence, revert to some pedestrian proofs of Equivalence here
 and there, without the need for the Measure class.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Binary/ZBinary.v       | 2 +-
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0d8f8bf5d4..516827616f 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -12,7 +12,7 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import ZArith.
+Require Import ZArith_base.
 
 Local Open Scope Z_scope.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 410af329db..f752c19761 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -36,8 +36,8 @@ Hint Rewrite
 Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
-Instance Z_measure: @Measure Z.t Z Z.to_Z.
 Instance eq_equiv : Equivalence Z.eq.
+Proof. unfold Z.eq. firstorder. Qed.
 
 Obligation Tactic := zcongruence.
 
-- 
cgit v1.2.3