Une entrée spéciale "annot" pour les piquants

Positionnement du scope type_scope à certains endroits bien choisis


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

4 files changed, 22 insertions, 11 deletions

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 52e1328b5..06f28b503 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -12,15 +12,21 @@ Require Export Datatypes.
 
 (** Symbolic notations for things in [Datatypes.v] *)
 
-Infix LEFTA 4 "+" sum : type_scope.
-Infix RIGHTA 3 "*" prod : type_scope.
+Arguments Scope sum [type_scope type_scope].
+Arguments Scope prod [type_scope type_scope].
+
+Infix "+" sum (at level 4, left associativity) : type_scope.
+Infix "*" prod (at level 3, right associativity) : type_scope.
+
 Notation "( x , y )" := (pair ? ? x y) (at level 0).
 Notation Fst := (fst ? ?).
 Notation Snd := (snd ? ?).
 
+Arguments Scope option [ type_scope ].
+
 (** Parsing only of things in [Datatypes.v] *)
 
-Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing).
-Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing).
-Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing).
+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/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fda1cde03..2ad45477f 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -12,7 +12,7 @@ Require Export Logic.
 
 (** Symbolic notations for things in [Logic.v] *)
 
-Notation "< P , Q > { p , q }" := (conj P Q p q) (at level 1).
+Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
 
 Notation "~ x" := (not x) (at level 5, right associativity).
 Notation "x = y" := (eq ? x y) (at level 5, no associativity).
@@ -42,5 +42,5 @@ Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
 
 (** Parsing only of things in [Logic.v] *)
 
-Notation "< A > 'All' ( P )" := (all A P) (at level 1, only parsing).
-Notation "< A > x = y" := (eq A x y) (at level 1, x at level 0, only parsing).
+Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing).
+Notation "< A > x = y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing).
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 0264df84b..ed915d119 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -34,7 +34,7 @@ Notation "'EXT' x | p & q"     := (exT2 ? [x]p [x]q)
 (** Parsing only of things in [Logic_type.v] *)
 
 Notation "< A > x == y"  := (eqT A x y)
-   (at level 1, x at level 0, only parsing).
+   (A annot, at level 1, x at level 0, only parsing).
 
 Notation "< A > x === y" := (identityT A x y)
-   (at level 1, x at level 0, only parsing).
+   (A annot, at level 1, x at level 0, only parsing).
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index c3934e7b8..9d868cb54 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -24,13 +24,18 @@ Notation Except := (except ?).
 Notation Error := (error ?).
 Notation Value := (value ?).
 
+Arguments Scope sig [type_scope type_scope].
+Arguments Scope sig2 [type_scope type_scope type_scope].
+
 Notation "{ x : A  |  P }"       := (sig A [x:A]P)          (at level 1).
 Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q)  (at level 1).
 
+Arguments Scope sigS [type_scope type_scope].
+Arguments Scope sigS2 [type_scope type_scope type_scope].
+
 Notation "{ x : A  &  P }"       := (sigS A [x:A]P)         (at level 1).
 Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1).
 
-
 (** Extra factorization of parsing rules *)
 
 (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)