Definitions of positive, N, Z moved in Numbers/BinNums.v

 In the coming reorganisation, the name Z in BinInt will be a
 module containing all code and properties about binary integers.
 The inductive type Z hence cannot be at the same location.
 Same for N and positive. Apart for this naming constraint, it
 also have advantages : presenting the three types at once is
 clearer, and we will be able to refer to N in BinPos (for instance
 for output type of a predecessor function on positive).

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

2 files changed, 19 insertions, 20 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index ad3781832..6e5443e35 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -7,25 +7,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Export BinNums BinPos Pnat.
+Require Import BinNat Plus Mult.
+
 (***********************************************************)
 (** * Binary Integers *)
-(** Initial author: Pierre Crégut, CNET, Lannion, France *)
 (***********************************************************)
 
-Require Export BinPos Pnat.
-Require Import BinNat Plus Mult.
-
-Inductive Z : Set :=
-  | Z0 : Z
-  | Zpos : positive -> Z
-  | Zneg : positive -> Z.
+(** Initial author: Pierre Crégut, CNET, Lannion, France *)
 
+(** The type [Z] and its constructors [Z0] and [Zpos] and [Zneg]
+    are now defined in [BinNums.v] *)
 
-(** Automatically open scope positive_scope for the constructors of Z *)
-Delimit Scope Z_scope with Z.
-Bind Scope Z_scope with Z.
-Arguments Scope Zpos [positive_scope].
-Arguments Scope Zneg [positive_scope].
+Local Open Scope Z_scope.
 
 (*************************************)
 (** * Basic operations *)
@@ -53,8 +47,6 @@ Definition Zdouble (x:Z) :=
     | Zneg p => Zneg p~0
   end.
 
-Open Local Scope positive_scope.
-
 Fixpoint ZPminus (x y:positive) {struct y} : Z :=
   match x, y with
     | p~1, q~1 => Zdouble (ZPminus p q)
@@ -66,9 +58,7 @@ Fixpoint ZPminus (x y:positive) {struct y} : Z :=
     | 1, q~1 => Zneg q~0
     | 1, q~0 => Zneg (Pdouble_minus_one q)
     | 1, 1 => Z0
-  end.
-
-Close Local Scope positive_scope.
+  end%positive.
 
 (** ** Addition on integers *)
 
@@ -191,8 +181,6 @@ Definition Zplus' (x y:Z) :=
     | Zneg x', Zneg y' => Zneg (x' + y')
   end.
 
-Open Local Scope Z_scope.
-
 (**********************************************************************)
 (** ** Inductive specification of Z *)
 
@@ -1050,3 +1038,13 @@ Definition Z_of_N (x:N) :=
     | N0 => Z0
     | Npos p => Zpos p
   end.
+
+(** Compatibility Notations *)
+
+Notation Z := Z (only parsing).
+Notation Z_rect := Z_rect (only parsing).
+Notation Z_rec := Z_rec (only parsing).
+Notation Z_ind := Z_ind (only parsing).
+Notation Z0 := Z0 (only parsing).
+Notation Zpos := Zpos (only parsing).
+Notation Zneg := Zneg (only parsing).
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 10a071c80..05df86880 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -10,6 +10,7 @@
     These are the basic modules, required by [Omega] and [Ring] for instance.
     The full library is [ZArith]. *)
 
+Require Export BinNums.
 Require Export BinPos.
 Require Export BinNat.
 Require Export BinInt.