Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

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

1 files changed, 4 insertions, 23 deletions

diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 45fcc17be..d91843aef 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -33,29 +33,10 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
 (**********************************************************************)
 (** * Boolean comparisons of binary integers *)
 
-Definition Zle_bool (x y:Z) :=
-  match x ?= y with
-    | Gt => false
-    | _ => true
-  end.
-
-Definition Zge_bool (x y:Z) :=
-  match x ?= y with
-    | Lt => false
-    | _ => true
-  end.
-
-Definition Zlt_bool (x y:Z) :=
-  match x ?= y with
-    | Lt => true
-    | _ => false
-  end.
-
-Definition Zgt_bool (x y:Z) :=
-  match x ?= y with
-    | Gt => true
-    | _ => false
-  end.
+Notation Zle_bool := Z.leb (only parsing).
+Notation Zge_bool := Z.geb (only parsing).
+Notation Zlt_bool := Z.ltb (only parsing).
+Notation Zgt_bool := Z.gtb (only parsing).
 
 Definition Zeq_bool (x y:Z) :=
   match x ?= y with