Intégration DatatypesSyntax à Datatypes

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

1 files changed, 0 insertions, 25 deletions

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).
-].