BinNatDef containing all functions of BinNat, misc adaptations in BinPos

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

2 files changed, 18 insertions, 16 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 67d193a6d..4ef91362f 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -34,7 +34,7 @@ Module Pos
  <: UsualDecidableTypeFull
  <: TotalOrder.
 
-(** * The definitions of operations are now in a separate file *)
+(** * Definitions of operations, now in a separate file *)
 
 Include BinPosDef.Pos.
 
@@ -42,10 +42,27 @@ Include BinPosDef.Pos.
 Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
 Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p.
 
+(** * Logical Predicates *)
+
 Definition eq := @Logic.eq t.
 Definition eq_equiv := @eq_equivalence t.
 Include BackportEq.
 
+Definition lt x y := (x ?= y) = Lt.
+Definition gt x y := (x ?= y) = Gt.
+Definition le x y := (x ?= y) <> Gt.
+Definition ge x y := (x ?= y) <> Lt.
+
+Infix "<=" := le : positive_scope.
+Infix "<" := lt : positive_scope.
+Infix ">=" := ge : positive_scope.
+Infix ">" := gt : positive_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
+Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
+
 (**********************************************************************)
 (** * Properties of operations over positive numbers *)
 
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 10c882188..cf7e450f4 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -265,21 +265,6 @@ Definition compare x y := compare_cont x y Eq.
 
 Infix "?=" := compare (at level 70, no associativity) : positive_scope.
 
-Definition lt x y := (x ?= y) = Lt.
-Definition gt x y := (x ?= y) = Gt.
-Definition le x y := (x ?= y) <> Gt.
-Definition ge x y := (x ?= y) <> Lt.
-
-Infix "<=" := le : positive_scope.
-Infix "<" := lt : positive_scope.
-Infix ">=" := ge : positive_scope.
-Infix ">" := gt : positive_scope.
-
-Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
-Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
-Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
-Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
-
 Definition min p p' :=
  match p ?= p' with
  | Lt | Eq => p