Intégration DatatypesSyntax à Datatypes

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

2 files changed, 23 insertions, 25 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index aed8c53f5e..a012d4e36d 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -44,22 +44,45 @@ 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
     := inl : A -> (sum A B)
      | inr : B -> (sum A B).
 
+Infix "+" sum (at level 4, left associativity) : 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)] *)
 
 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) (at level 3, right associativity) : type_scope
+  V8only (at level 30, left associativity).
+
+Notation "( x , y )" := (pair ? ? x y) (at level 0)
+  V8only "x , y" (at level 150, left associativity).
+
 Section projections.
    Variables A,B:Set.
    Definition fst := [p:(prod A B)]Cases p of (pair x y) => x end.
    Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end.
 End projections. 
 
+Notation Fst := (fst ? ?).
+Notation Snd := (snd ? ?).
+
 Hints Resolve pair inl inr : core v62.
+
+(** Parsing only of things in [Datatypes.v] *)
+V7only[
+Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot).
+Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot).
+Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot).
+].
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 0ba1a58848..a4b6a57aae 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -8,28 +8,3 @@
 
 (*i $Id$ i*)
 
-Require Export Datatypes.
-
-(** Symbolic notations for things in [Datatypes.v] *)
-
-Arguments Scope sum [type_scope type_scope].
-Arguments Scope prod [type_scope type_scope].
-
-Infix LEFTA 4 "+" sum : type_scope.
-Notation "x * y" := (prod x y) (at level 3, right associativity) : type_scope
-  V8only (at level 30, left associativity).
-
-Notation "( x , y )" := (pair ? ? x y) (at level 0)
-  V8only "x , y" (at level 150, left associativity).
-Notation Fst := (fst ? ?).
-Notation Snd := (snd ? ?).
-
-Arguments Scope option [ type_scope ].
-
-(** Parsing only of things in [Datatypes.v] *)
-
-V7only[
-Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot).
-Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot).
-Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot).
-].