ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType

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

2 files changed, 3 insertions, 4 deletions

diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 487b1d0cc..3d4430b9e 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -176,8 +176,7 @@ Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
 
 Module Type UsualIsEq (E:UsualEq) <: IsEq E.
  (* No Instance syntax to avoid saturating the Equivalence tables *)
- Lemma eq_equiv : Equivalence E.eq.
- Proof. exact eq_equivalence. Qed.
+ Definition eq_equiv : Equivalence E.eq := eq_equivalence.
 End UsualIsEq.
 
 Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index 56f1d5ded..d7c0deb94 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -14,7 +14,7 @@
 (* $Id$ *)
 
 Require Import Orders NatOrderedType POrderedType NOrderedType
- ZOrderedType RelationPairs EqualitiesFacts.
+ ZBinary RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
@@ -24,7 +24,7 @@ Require Import Orders NatOrderedType POrderedType NOrderedType
 Module Nat_as_OT := NatOrderedType.Nat_as_OT.
 Module Positive_as_OT := POrderedType.Positive_as_OT.
 Module N_as_OT := NOrderedType.N_as_OT.
-Module Z_as_OT := ZOrderedType.Z_as_OT.
+Module Z_as_OT := ZBinary.Z.
 
 (** An OrderedType can now directly be seen as a DecidableType *)