Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

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

2 files changed, 14 insertions, 14 deletions

diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 14d34f1eb..8e72bd611 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 Require Export RelationClasses.
+Require Import Bool Morphisms Setoid.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -165,6 +166,18 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
 Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
  := E <+ HasEqBool2Dec.
 
+(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType).
+
+Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
+Proof.
+intros x x' Exx' y y' Eyy'.
+apply eq_true_iff_eq.
+now rewrite 2 eqb_eq, Exx', Eyy'.
+Qed.
+
+End BoolEqualityFacts.
 
 
 (** * UsualDecidableType
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index d9b1d76fd..d8a1b7581 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -8,21 +8,8 @@
 
 Require Import Equalities Bool SetoidList RelationPairs.
 
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
-
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
-
-Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
-Proof.
-intros x x' Exx' y y' Eyy'.
-apply eq_true_iff_eq.
-rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
-Qed.
-
-End BoolEqualityFacts.
-
-
 (** * Keys and datas used in FMap *)
+
 Module KeyDecidableType(Import D:DecidableType).
 
  Section Elt.