Bind et Delimit pour nat

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

2 files changed, 10 insertions, 1 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cb2c272846..8ec5b7c905 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -30,6 +30,10 @@ Add Printing If bool.
 Inductive nat : Set := O : nat 
                      | S : nat->nat.
 
+Delimits Scope nat_scope with N.
+Bind Scope nat_scope with nat.
+Arguments Scope S [ nat_scope ].
+
 (** [Empty_set] has no inhabitant *)
 
 Inductive Empty_set:Set :=.
@@ -46,7 +50,9 @@ Hints Resolve refl_identity : core v62.
 
 Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A).
 
+(*
 Arguments Scope option [ type_scope ].
+*)
 
 (** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
@@ -55,7 +61,9 @@ Inductive sum [A,B:Set] : Set
      | inr : B -> (sum A B).
 
 Notation "x + y" := (sum x y) : type_scope.
+(*
 Arguments Scope sum [type_scope type_scope].
+*)
 
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
@@ -63,7 +71,9 @@ Arguments Scope sum [type_scope type_scope].
 Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B).
 Add Printing Let prod.
 
+(*
 Arguments Scope prod [type_scope type_scope].
+*)
 
 Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y )" := (pair ? ? x y) V8only "x , y".
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 55e44d28d2..2df5229881 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -199,4 +199,3 @@ Infix NONA 5 ">" gt : nat_scope.
 V7only [
 End nat_scope.
 ].
-Delimits Scope nat_scope with N.