Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

5 files changed, 23 insertions, 11 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index e6a14938..b4582d51 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinNat.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+(*i $Id: BinNat.v 8685 2006-04-06 13:22:02Z letouzey $ i*)
 
 Require Import BinPos.
+Unset Boxed Definitions.
 
 (**********************************************************************)
 (** Binary natural numbers *)
@@ -21,10 +22,10 @@ Inductive N : Set :=
 
 Delimit Scope N_scope with N.
 
-(** Automatically open scope N_scope for the constructors of N *)
+(** Automatically open scope positive_scope for the constructors of N *)
 
 Bind Scope N_scope with N.
-Arguments Scope Npos [N_scope].
+Arguments Scope Npos [positive_scope].
 
 Open Local Scope N_scope.
 
@@ -32,7 +33,7 @@ Open Local Scope N_scope.
 
 Definition Ndouble_plus_one x :=
   match x with
-  | N0 => Npos 1%positive
+  | N0 => Npos 1
   | Npos p => Npos (xI p)
   end.
 
@@ -47,7 +48,7 @@ Definition Ndouble n := match n with
 
 Definition Nsucc n :=
   match n with
-  | N0 => Npos 1%positive
+  | N0 => Npos 1
   | Npos p => Npos (Psucc p)
   end.
 
@@ -57,7 +58,7 @@ Definition Nplus n m :=
   match n, m with
   | N0, _ => m
   | _, N0 => n
-  | Npos p, Npos q => Npos (p + q)%positive
+  | Npos p, Npos q => Npos (p + q)
   end.
 
 Infix "+" := Nplus : N_scope.
@@ -68,7 +69,7 @@ Definition Nmult n m :=
   match n, m with
   | N0, _ => N0
   | _, N0 => N0
-  | Npos p, Npos q => Npos (p * q)%positive
+  | Npos p, Npos q => Npos (p * q)
   end.
 
 Infix "*" := Nmult : N_scope.
@@ -154,7 +155,7 @@ Qed.
 
 (** Properties of multiplication *)
 
-Theorem Nmult_1_l : forall n:N, Npos 1%positive * n = n.
+Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
 Proof.
 destruct n; reflexivity.
 Qed.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index fffb10c1..513a67c2 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinPos.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+(*i $Id: BinPos.v 6699 2005-02-07 14:30:08Z coq $ i*)
+
+Unset Boxed Definitions.
 
 (**********************************************************************)
 (** Binary positive numbers *)
@@ -39,6 +41,8 @@ Fixpoint Psucc (x:positive) : positive :=
 
 (** Addition *)
 
+Set Boxed Definitions.
+
 Fixpoint Pplus (x y:positive) {struct x} : positive :=
   match x, y with
   | xI x', xI y' => xO (Pplus_carry x' y')
@@ -65,6 +69,8 @@ Fixpoint Pplus (x y:positive) {struct x} : positive :=
   | xH, xH => xI xH
   end.
 
+Unset Boxed Definitions.
+
 Infix "+" := Pplus : positive_scope.
 
 Open Local Scope positive_scope.
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index b1bdaaf0..2f066efa 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: NArith.v,v 1.2.2.1 2004/07/16 19:31:07 herbelin Exp $ *)
+(* $Id: NArith.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (** Library for binary natural numbers *)
 
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
index f5bbb1c9..88abc700 100644
--- a/theories/NArith/Pnat.v
+++ b/theories/NArith/Pnat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Pnat.v,v 1.3.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+(*i $Id: Pnat.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 Require Import BinPos.
 
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
new file mode 100644
index 00000000..83eed970
--- /dev/null
+++ b/theories/NArith/intro.tex
@@ -0,0 +1,5 @@
+\section{Binary positive and non negative integers : NArith}\label{NArith}
+
+Here are defined various arithmetical notions and their properties,
+similar to those of {\tt Arith}.
+