ouverture du bon scope (positive_scope) derriere le constructeur Npos de N

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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 6676ea3bf4..02e6b48d14 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -22,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.
 
@@ -33,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.
 
@@ -48,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.
 
@@ -58,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.
@@ -69,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.
@@ -155,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.