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

14 files changed, 163 insertions, 118 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ac1aa1879..0f3d1bab2 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -91,12 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
 let arith_dir = ["Coq";"Arith"]
 let arith_modules = [arith_dir]
 
+let numbers_dir = [ "Coq";"Numbers"]
 let parith_dir = ["Coq";"PArith"]
-
 let narith_dir = ["Coq";"NArith"]
-
 let zarith_dir = ["Coq";"ZArith"]
-let zarith_base_modules = [parith_dir;narith_dir;zarith_dir]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
 
 let init_dir = ["Coq";"Init"]
 let init_modules = [
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index c8d324730..ab63f7bf0 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -194,7 +194,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z)  :=
       | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
     end.
 
-Require Import Tauto.
+Require Import Tauto BinNums.
 
 Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
   List.map  (fun x => x::nil) (xnormalise t).
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d410d6a5c..877d468fd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -220,6 +220,8 @@ struct
       ["Coq";"Reals" ; "Rpow_def"];
       ["LRing_normalise"]]
 
+  let bin_module = [["Coq";"Numbers";"BinNums"]]
+
   let r_modules =
     [["Coq";"Reals" ; "Rdefinitions"];
      ["Coq";"Reals" ; "Rpow_def"]]
@@ -231,6 +233,7 @@ struct
 
   let init_constant = gen_constant_in_modules "ZMicromega" init_modules
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
+  let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
   let r_constant = gen_constant_in_modules "ZMicromega" r_modules
   (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
 
@@ -249,31 +252,26 @@ struct
   let coq_S = lazy (init_constant "S")
   let coq_nat = lazy (init_constant "nat")
 
-  let coq_NO = lazy
-   (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]]  "N0")
-  let coq_Npos = lazy
-   (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]]  "Npos")
-   (* let coq_n = lazy (constant "N")*)
+  let coq_N0 = lazy (bin_constant "N0")
+  let coq_Npos = lazy (bin_constant "Npos")
+
+  let coq_pair = lazy (init_constant "pair")
+  let coq_None = lazy (init_constant "None")
+  let coq_option = lazy (init_constant "option")
 
-  let coq_pair = lazy (constant "pair")
-  let coq_None = lazy (constant "None")
-  let coq_option = lazy (constant "option")
-  let coq_positive = lazy (constant "positive")
-  let coq_xH = lazy (constant "xH")
-  let coq_xO = lazy (constant "xO")
-  let coq_xI = lazy (constant "xI")
+  let coq_positive = lazy (bin_constant "positive")
+  let coq_xH = lazy (bin_constant "xH")
+  let coq_xO = lazy (bin_constant "xO")
+  let coq_xI = lazy (bin_constant "xI")
 
-  let coq_N0 = lazy (constant "N0")
-  let coq_N0 = lazy (constant "Npos")
+  let coq_Z = lazy (bin_constant "Z")
+  let coq_ZERO = lazy (bin_constant "Z0")
+  let coq_POS = lazy (bin_constant "Zpos")
+  let coq_NEG = lazy (bin_constant "Zneg")
 
-  let coq_Z = lazy (constant "Z")
   let coq_Q = lazy (constant "Q")
   let coq_R = lazy (constant "R")
 
-  let coq_ZERO = lazy (constant  "Z0")
-  let coq_POS = lazy (constant  "Zpos")
-  let coq_NEG = lazy (constant  "Zneg")
-
   let coq_Build_Witness = lazy (constant "Build_Witness")
 
   let coq_Qmake = lazy (constant "Qmake")
@@ -496,11 +494,6 @@ struct
 
   let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
 
-  let rec dump_n x =
-   match x with
-    | Mc.N0 -> Lazy.force coq_NO
-    | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |])
-
   let rec pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
 
   let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 2b5a3e7c8..4b8b706d4 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -180,21 +180,24 @@ let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul")
 let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp")
 let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow")
 
-let tlist = lazy (gen_constant "CC" ["Lists";"List"] "list")
-let lnil = lazy (gen_constant "CC" ["Lists";"List"] "nil")
-let lcons = lazy (gen_constant "CC" ["Lists";"List"] "cons")
+let datatypes = ["Init";"Datatypes"]
+let binnums = ["Numbers";"BinNums"]
 
-let tz = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z")
-let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0")
-let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos")
-let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg")
+let tlist = lazy (gen_constant "CC" datatypes "list")
+let lnil = lazy (gen_constant "CC" datatypes "nil")
+let lcons = lazy (gen_constant "CC" datatypes "cons")
 
-let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI")
-let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO")
-let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH")
+let tz = lazy (gen_constant "CC" binnums "Z")
+let z0 = lazy (gen_constant "CC" binnums "Z0")
+let zpos = lazy (gen_constant "CC" binnums "Zpos")
+let zneg = lazy(gen_constant "CC" binnums "Zneg")
 
-let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0")
-let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos")
+let pxI = lazy(gen_constant "CC" binnums "xI")
+let pxO = lazy(gen_constant "CC" binnums "xO")
+let pxH = lazy(gen_constant "CC" binnums "xH")
+
+let nN0 = lazy (gen_constant "CC" binnums "N0")
+let nNpos = lazy(gen_constant "CC" binnums "Npos")
 
 let mkt_app name l =  mkApp (Lazy.force name, Array.of_list l)
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index a520ce2d4..cddc5472d 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -36,7 +36,7 @@ let l_true_equals_true =
         [|data_constant "bool";data_constant "true"|]))
 
 let pos_constant =
-  Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"]
+  Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index cf0253d1f..f8bce8f79 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -22,17 +22,18 @@ exception Non_closed_number
 
 open Libnames
 open Glob_term
+
+let binnums = ["Coq";"Numbers";"BinNums"]
+
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let positive_module = ["Coq";"PArith";"BinPos"]
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
-let positive_path = make_path positive_module "positive"
+let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_mind dir id
 
-let positive_kn =
-  make_kn (make_dir positive_module) (id_of_string "positive")
+let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
@@ -82,7 +83,7 @@ let uninterp_positive p =
 (************************************************************************)
 
 let _ = Notation.declare_numeral_interpreter "positive_scope"
-  (positive_path,positive_module)
+  (positive_path,binnums)
   interp_positive
   ([GRef (dummy_loc, glob_xI);
     GRef (dummy_loc, glob_xO);
@@ -94,15 +95,14 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let binnat_module = ["Coq";"NArith";"BinNat"]
-let n_kn = make_kn (make_dir binnat_module) (id_of_string "N")
+let n_kn = make_kn (make_dir binnums) (id_of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
 let path_of_Npos = ((n_kn,0),2)
 let glob_N0 = ConstructRef path_of_N0
 let glob_Npos = ConstructRef path_of_Npos
 
-let n_path = make_path binnat_module "N"
+let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
   if n <> zero then
@@ -134,7 +134,7 @@ let uninterp_n p =
 (* Declaring interpreters and uninterpreters for N *)
 
 let _ = Notation.declare_numeral_interpreter "N_scope"
-  (n_path,binnat_module)
+  (n_path,binnums)
   n_of_int
   ([GRef (dummy_loc, glob_N0);
     GRef (dummy_loc, glob_Npos)],
@@ -145,9 +145,8 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
 (* Parsing Z via scopes                                               *)
 (**********************************************************************)
 
-let binint_module = ["Coq";"ZArith";"BinInt"]
-let z_path = make_path binint_module "Z"
-let z_kn = make_kn (make_dir binint_module) (id_of_string "Z")
+let z_path = make_path binnums "Z"
+let z_kn = make_kn (make_dir binnums) (id_of_string "Z")
 let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
@@ -183,7 +182,7 @@ let uninterp_z p =
 (* Declaring interpreters and uninterpreters for Z *)
 
 let _ = Notation.declare_numeral_interpreter "Z_scope"
-  (z_path,binint_module)
+  (z_path,binnums)
   z_of_int
   ([GRef (dummy_loc, glob_ZERO);
     GRef (dummy_loc, glob_POS);
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.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
new file mode 100644
index 000000000..69754f144
--- /dev/null
+++ b/theories/Numbers/BinNums.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Binary Numerical Datatypes *)
+
+Set Implicit Arguments.
+(* For compatibility, we will not use generic equality functions *)
+Local Unset Boolean Equality Schemes.
+
+Declare ML Module "z_syntax_plugin".
+
+(** [positive] is a datatype representing the strictly positive integers
+   in a binary way. Starting from 1 (represented by [xH]), one can
+   add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
+   Numbers in [positive] can also be denoted using a decimal notation;
+   e.g. [6%positive] abbreviates [xO (xI xH)] *)
+
+Inductive positive : Set :=
+  | xI : positive -> positive
+  | xO : positive -> positive
+  | xH : positive.
+
+Delimit Scope positive_scope with positive.
+Bind Scope positive_scope with positive.
+Arguments Scope xO [positive_scope].
+Arguments Scope xI [positive_scope].
+
+(** [N] is a datatype representing natural numbers in a binary way,
+    by extending the [positive] datatype with a zero.
+    Numbers in [N] can also be denoted using a decimal notation;
+    e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+
+Inductive N : Set :=
+  | N0 : N
+  | Npos : positive -> N.
+
+Delimit Scope N_scope with N.
+Bind Scope N_scope with N.
+Arguments Scope Npos [positive_scope].
+
+(** [Z] is a datatype representing the integers in a binary way.
+    An integer is either zero or a strictly positive number
+    (coded as a [positive]) or a strictly negative number
+    (whose opposite is stored as a [positive] value).
+    Numbers in [Z] can also be denoted using a decimal notation;
+    e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+
+Inductive Z : Set :=
+  | Z0 : Z
+  | Zpos : positive -> Z
+  | Zneg : positive -> Z.
+
+Delimit Scope Z_scope with Z.
+Bind Scope Z_scope with Z.
+Arguments Scope Zpos [positive_scope].
+Arguments Scope Zneg [positive_scope].
diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget
index baefbd252..c69af03fc 100644
--- a/theories/Numbers/vo.itarget
+++ b/theories/Numbers/vo.itarget
@@ -1,3 +1,4 @@
+BinNums.vo
 BigNumPrelude.vo
 Cyclic/Abstract/CyclicAxioms.vo
 Cyclic/Abstract/NZCyclic.vo
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index ec18d8dc5..badae225f 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -7,32 +7,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Declare ML Module "z_syntax_plugin".
+Require Export BinNums.
 
 (**********************************************************************)
-(** * Binary positive numbers *)
+(** * Binary positive numbers, operations and properties *)
 (**********************************************************************)
 
 (** Initial development by Pierre Crégut, CNET, Lannion, France *)
 
-Inductive positive : Set :=
-| xI : positive -> positive
-| xO : positive -> positive
-| xH : positive.
-
-(** Declare binding key for scope positive_scope *)
-
-Delimit Scope positive_scope with positive.
-
-(** Automatically open scope positive_scope for type positive, xO and xI *)
-
-Bind Scope positive_scope with positive.
-Arguments Scope xO [positive_scope].
-Arguments Scope xI [positive_scope].
+(** The type [positive] and its constructors [xI] and [xO] and [xH]
+    are now defined in [BinNums.v] *)
 
 (** Postfix notation for positive numbers, allowing to mimic
     the position of bits in a big-endian representation.
-    For instance, we can write 1~1~0 instead of (xO (xI xH))
+    For instance, we can write [1~1~0] instead of [(xO (xI xH))]
     for the number 6 (which is 110 in binary notation).
 *)
 
@@ -42,12 +30,8 @@ Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Local Open Scope positive_scope.
-
-(* In the current file, [xH] cannot yet be written as [1], since the
-   interpretation of positive numerical constants is not available
-   yet. We fix this here with an ad-hoc temporary notation. *)
-
-Local Notation "1" := xH (at level 7).
+Local Unset Boolean Equality Schemes.
+Local Unset Case Analysis Schemes.
 
 (**********************************************************************)
 (** * Operations over positive numbers *)
@@ -1599,3 +1583,13 @@ Proof.
  apply Pmult_le_mono_l.
  apply Ple_lteq; left. rewrite xI_succ_xO. apply Plt_succ_r, IHp.
 Qed.
+
+(** Compatibility notations *)
+
+Notation positive := positive (only parsing).
+Notation positive_rect := positive_rect (only parsing).
+Notation positive_rec := positive_rec (only parsing).
+Notation positive_ind := positive_ind (only parsing).
+Notation xI := xI (only parsing).
+Notation xO := xO (only parsing).
+Notation xH := xH (only parsing).
diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v
index 8688c5013..e2bec88af 100644
--- a/theories/PArith/PArith.v
+++ b/theories/PArith/PArith.v
@@ -8,4 +8,4 @@
 
 (** Library for positive natural numbers *)
 
-Require Export BinPos Pnat Pminmax Psqrt Pgcd POrderedType.
+Require Export BinNums BinPos Pnat Pminmax Psqrt Pgcd POrderedType.
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.