ZArith_base, Zbool, Bool_nat

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

17 files changed, 164 insertions, 89 deletions

diff --git a/.depend.coq b/.depend.coq
index 32a312384c..3fb071f885 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -4,7 +4,7 @@ contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/R
 contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
 contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
-contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/ZArith/ZArith.vo theories/Bool/Sumbool.vo
+contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/ZArith/ZArith.vo theories/Arith/Bool_nat.vo theories/Bool/Sumbool.vo
 contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
 contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo theories/ZArith/Zwf.vo contrib/correctness/Arrays.vo
@@ -18,14 +18,14 @@ contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring
 contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Quote.vo: contrib/ring/Quote.v
 contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
-contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
-contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo
+contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo theories/Arith/Minus.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
@@ -115,19 +115,21 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
-theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
-theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
-theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
+theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/ZArith_base.vo theories/Bool/Sumbool.vo
+theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
+theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
 theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
 theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo
 theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo
 theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
 theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
-theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
+theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zbool.vo
 theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
 theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
 theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
@@ -136,6 +138,7 @@ theories/Bool/DecBool.vo: theories/Bool/DecBool.v
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
+theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo
 theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/ArithSyntax.vo
diff --git a/Makefile b/Makefile
index 84c8059581..24f99933cf 100644
--- a/Makefile
+++ b/Makefile
@@ -439,6 +439,7 @@ ARITHVO=theories/Arith/ArithSyntax.vo \
 	theories/Arith/EqNat.vo         theories/Arith/Peano_dec.vo   \
 	theories/Arith/Euclid.vo        theories/Arith/Plus.vo        \
 	theories/Arith/Wf_nat.vo  	theories/Arith/Max.vo	      \
+	theories/Arith/Bool_nat.vo
 #	theories/Arith/Div.vo 
 
 SORTINGVO=theories/Sorting/Heap.vo \
@@ -456,7 +457,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
 	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
-	 theories/ZArith/Zwf.vo
+	 theories/ZArith/Zwf.vo		theories/ZArith/ZArith_base.vo \
+	 theories/ZArith/Zbool.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v
index 026390a01d..d618e235a2 100644
--- a/contrib/correctness/ProgBool.v
+++ b/contrib/correctness/ProgBool.v
@@ -10,24 +10,10 @@
 
 (* $Id$ *)
 
-Require Export Compare_dec.
-Require Export Peano_dec.
 Require ZArith.
+Require Bool_nat.
 Require Sumbool.
 
-(* Programs use the booleans of type "bool", so we tranform any decidability
- * proof, in type sumbool, into a function returning a boolean with the
- * correct specification, through the following function:
- *)
-
-Definition bool_of_sumbool : 
-  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
-Proof.
-Intros A B H.
-Elim H; [ Intro; Exists true; Assumption
-        | Intro; Exists false; Assumption ].
-Save.
-
 Definition annot_bool :
   (b:bool) { b':bool | if b' then b=true else b=false }.
 Proof.
@@ -78,45 +64,3 @@ Case b; Intro.
 Exists false; Auto. Exists true; Auto.
 Save.
 
-
-(* Application: the decidability of equality and order relations over
- * type Z give some boolean functions with the adequate specification.
- * For instance, Z_lt_ge_bool has type:
- * 
- *        (x,y:Z){b:bool | if b then `x < y` else `x >= y`}
- *)
-
-Definition Z_lt_ge_bool := [x,y:Z](bool_of_sumbool ? ? (Z_lt_ge_dec x y)).
-Definition Z_ge_lt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_ge_lt_dec x y)).
-
-Definition Z_le_gt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_le_gt_dec x y)).
-Definition Z_gt_le_bool := [x,y:Z](bool_of_sumbool ? ? (Z_gt_le_dec x y)).
-
-Definition Z_eq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_eq_dec x y)).
-Definition Z_noteq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_noteq_dec x y)).
-
-Definition Zeven_odd_bool := [x:Z](bool_of_sumbool ? ? (Zeven_odd_dec x)).
-
-(* ... and similarly for type nat *)
-
-Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
-Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := 
-  [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
-
-Definition nat_lt_ge_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (lt_ge_dec x y)).
-Definition nat_ge_lt_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (lt_ge_dec x y))).
-
-Definition nat_le_gt_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (le_gt_dec x y)).
-Definition nat_gt_le_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (le_gt_dec x y))).
-
-Definition nat_eq_bool :=
-  [x,y:nat](bool_of_sumbool ? ? (eq_nat_dec x y)).
-Definition nat_noteq_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (eq_nat_dec x y))).
-
-Definition zerop_bool := [x:nat](bool_of_sumbool ? ? (zerop x)).
-Definition notzerop_bool := [x:nat](bool_of_sumbool ? ? (notzerop x)).
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 7da167623c..77906873d1 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -15,7 +15,21 @@
 
 (* $Id$ *)
 
-Require Export ZArith.
+(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+Require Export fast_integer.
+Require Export zarith_aux.
+Require Export auxiliary.
+Require Export Zsyntax.
+Require Export ZArith_dec.
+Require Export Zmisc.
+Require Export Wf_Z.
+
+Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
+  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
+  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+
+Require Export Zhints.
+
 (* The constant minus is required in coq_omega.ml *)
 Require Export Minus.
 
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 2de8611764..65fd1bc64a 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -11,7 +11,7 @@
 (* Instantiation of the Ring tactic for the binary integers of ZArith *)
 
 Require Export ArithRing.
-Require Export ZArith.
+Require Export ZArith_base.
 Require Eqdep_dec.
 
 Definition Zeq := [x,y:Z]
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 41e29d38e2..f0ccfb886e 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -9,7 +9,7 @@
 Require Arith.
 Require PolyList.
 Require Bool.
-Require ZArith.
+Require ZArith_base.
 
 (* \subsection{Définition des types} *)
 
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
new file mode 100644
index 0000000000..872c314f16
--- /dev/null
+++ b/theories/Arith/Bool_nat.v
@@ -0,0 +1,38 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Export Compare_dec.
+Require Export Peano_dec.
+Require Sumbool.
+
+(** The decidability of equality and order relations over
+    type [nat] give some boolean functions with the adequate specification. *)
+
+Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
+Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := 
+  [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
+
+Definition nat_lt_ge_bool := 
+  [x,y:nat](bool_of_sumbool (lt_ge_dec x y)).
+Definition nat_ge_lt_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))).
+
+Definition nat_le_gt_bool := 
+  [x,y:nat](bool_of_sumbool (le_gt_dec x y)).
+Definition nat_gt_le_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))).
+
+Definition nat_eq_bool :=
+  [x,y:nat](bool_of_sumbool (eq_nat_dec x y)).
+Definition nat_noteq_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))).
+
+Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)).
+Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)).
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 8172129090..84e74f86bb 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -62,3 +62,16 @@ Qed.
 End connectives.
 
 Hints Resolve sumbool_and sumbool_or sumbool_not : core.
+
+
+(** Any decidability function in type [sumbool] can be turned into a function
+    returning a boolean with the corresponding specification: *)
+
+Definition bool_of_sumbool : 
+  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
+Proof.
+Intros A B H.
+Elim H; [ Intro; Exists true; Assumption
+        | Intro; Exists false; Assumption ].
+Save.
+Implicits bool_of_sumbool.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 240efb6e40..f85b0bddd3 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -10,16 +10,13 @@
 
 (** Library for manipulating integers based on binary encoding *)
 
-Require Export fast_integer.
-Require Export zarith_aux.
-Require Export auxiliary.
-Require Export Zsyntax.
-Require Export ZArith_dec.
-Require Export Zmisc.
-Require Export Wf_Z.
+Require Export ZArith_base.
 
-Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
-  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
-  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+(** Extra modules using [Omega] or [Ring]. *)
 
-Require Export Zhints.
+Require Export Zcomplements.
+Require Export Zsqrt.
+Require Export Zpower.
+Require Export Zdiv.
+Require Export Zlogarithm.
+Require Export Zbool.
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
new file mode 100644
index 0000000000..e17bcbe2a4
--- /dev/null
+++ b/theories/ZArith/ZArith_base.v
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** Library for manipulating integers based on binary encoding.
+    These are the basic modules, required by [Omega] and [Ring] for instance. 
+    The full library is [ZArith]. *)
+
+Require Export fast_integer.
+Require Export zarith_aux.
+Require Export auxiliary.
+Require Export Zsyntax.
+Require Export ZArith_dec.
+Require Export Zmisc.
+Require Export Wf_Z.
+
+Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
+  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
+  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+
+Require Export Zhints.
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
new file mode 100644
index 0000000000..4e385c11ef
--- /dev/null
+++ b/theories/ZArith/Zbool.v
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require ZArith_base.
+Require Sumbool.
+
+(** The decidability of equality and order relations over
+    type [Z] give some boolean functions with the adequate specification. *)
+
+Definition Z_lt_ge_bool := [x,y:Z](bool_of_sumbool (Z_lt_ge_dec x y)).
+Definition Z_ge_lt_bool := [x,y:Z](bool_of_sumbool (Z_ge_lt_dec x y)).
+
+Definition Z_le_gt_bool := [x,y:Z](bool_of_sumbool (Z_le_gt_dec x y)).
+Definition Z_gt_le_bool := [x,y:Z](bool_of_sumbool (Z_gt_le_dec x y)).
+
+Definition Z_eq_bool := [x,y:Z](bool_of_sumbool (Z_eq_dec x y)).
+Definition Z_noteq_bool := [x,y:Z](bool_of_sumbool (Z_noteq_dec x y)).
+
+Definition Zeven_odd_bool := [x:Z](bool_of_sumbool (Zeven_odd_dec x)).
+
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index cba4aaca27..78f5370983 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require ZArith.
+Require ZArith_base.
 Require ZArithRing.
 Require Omega.
 Require Wf_nat.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 0c4feab084..c3ebf133de 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -19,7 +19,7 @@ Then only after proves the main required property.
 
 *)
 
-Require Export ZArith.
+Require Export ZArith_base.
 Require Omega.
 Require ZArithRing.
 Require Zcomplements.
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 336886b5a2..660a58ed60 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -19,7 +19,7 @@
     - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]
       i.e. [Log_nearest x] is the integer nearest from [Log x] *)
 
-Require ZArith.
+Require ZArith_base.
 Require Omega.
 Require Zcomplements.
 Require Zpower.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 02b8ebd51b..11ec071c11 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require ZArith.
+Require ZArith_base.
 Require Omega.
 Require Zcomplements.
 
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 9939f838f2..1a78c90dff 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -1,4 +1,14 @@
-Require Export ZArith.
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Omega.
 
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 386317e831..2994bac314 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require ZArith.
+Require ZArith_base.
 Require Export Wf_nat.
 
 (** Well-founded relations on Z. *)