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, 15 insertions, 20 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 3f256b40f..3e576a08b 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -6,33 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Export BinNums.
 Require Import BinPos.
 
 (**********************************************************************)
-(** Binary natural numbers *)
-
-Inductive N : Set :=
-  | N0 : N
-  | Npos : positive -> N.
-
-(** Declare binding key for scope positive_scope *)
-
-Delimit Scope N_scope with N.
-
-(** Automatically open scope positive_scope for the constructors of N *)
+(** * Binary natural numbers, operations and properties *)
+(**********************************************************************)
 
-Bind Scope N_scope with N.
-Arguments Scope Npos [positive_scope].
+(** The type [N] and its constructors [N0] and [Npos] are now
+    defined in [BinNums.v] *)
 
 Local Open Scope N_scope.
 
-(** Some local ad-hoc notation, since no interpretation of numerical
-  constants is available yet. *)
-
-Local Notation "0" := N0 : N_scope.
-Local Notation "1" := (Npos 1) : N_scope.
-Local Notation "2" := (Npos 2) : N_scope.
-
 Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }.
 Proof.
  destruct n; auto.
@@ -693,3 +678,12 @@ Proof.
  intros (m,H). now destruct m.
  exists 0. reflexivity.
 Qed.
+
+(** Compatibility notations *)
+
+Notation N := N (only parsing).
+Notation N_rect := N_rect (only parsing).
+Notation N_rec := N_rec (only parsing).
+Notation N_ind := N_ind (only parsing).
+Notation N0 := N0 (only parsing).
+Notation Npos := Npos (only parsing).
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 22c9012a7..6bfc323d6 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -8,6 +8,7 @@
 
 (** Library for binary natural numbers *)
 
+Require Export BinNums.
 Require Export BinPos.
 Require Export BinNat.
 Require Export Nnat.