PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only OrderedType

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

1 files changed, 5 insertions, 10 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 10f6d44f3..70c221027 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -16,6 +16,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import OrderedType.
+Require Import OrderedTypeEx.
 Require Import FMapInterface.
 
 Set Implicit Arguments.
@@ -36,9 +37,12 @@ Open Scope positive_scope.
   usual order (see [OrderedTypeEx]), we use here a lexicographic order 
   over bits, which is more natural here (lower bits are considered first). *)
 
-Module PositiveOrderedTypeBits <: OrderedType.
+Module PositiveOrderedTypeBits <: UsualOrderedType.
   Definition t:=positive.
   Definition eq:=@eq positive.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
 
   Fixpoint bits_lt (p q:positive) { struct p } : Prop := 
    match p, q with 
@@ -52,15 +56,6 @@ Module PositiveOrderedTypeBits <: OrderedType.
 
   Definition lt:=bits_lt.
 
-  Lemma eq_refl : forall x : t, eq x x.
-  Proof. red; auto. Qed.
-
-  Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof. red; auto. Qed.
-
-  Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof. red; intros; transitivity y; auto. Qed.
-
   Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
   Proof.
   induction x.