Nettoyage

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

1 files changed, 0 insertions, 11 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8ec5b7c90..03b7c06f0 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -50,10 +50,6 @@ 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 *)
 Inductive sum [A,B:Set] : Set
@@ -61,9 +57,6 @@ 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)] *)
@@ -71,10 +64,6 @@ 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".