Simplification

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

1 files changed, 10 insertions, 17 deletions

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 1fd9d9930..c3934e7b8 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -14,11 +14,9 @@ Require Specif.
 (** Symbolic notations for things in [Specif.v] *)
 
 (* At level 1 to factor with {x:A|P} etc *)
-Notation "{ A } + { B }" := (sumbool A B)
-  (at level 1, A at level 10, B at level 10).
+Notation "{ A } + { B }" := (sumbool A B) (at level 1).
 
-Notation "A + { B }" := (sumor A B)
-  (at level 4, B at level 10, left associativity).
+Notation "A + { B }" := (sumor A B) (at level 4, left associativity).
 
 Notation ProjS1 := (projS1 ? ?).
 Notation ProjS2 := (projS2 ? ?).
@@ -26,31 +24,26 @@ Notation Except := (except ?).
 Notation Error := (error ?).
 Notation Value := (value ?).
 
-Notation "{ x : A  |  P }"       := (sig A [x:A]P)
-  (at level 1, x at level 10).
+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).
 
-Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q)
-  (at level 1, x at level 10).
+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).
 
-Notation "{ x : A  &  P }"       := (sigS A [x:A]P)
-  (at level 1, x at level 10).
-
-Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q)
-  (at level 1, x at level 10).
 
 (** Extra factorization of parsing rules *)
 
 (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
 
 Notation "B + { x : A | P }"     := B + ({x:A | P})
-  (at level 4, x at level 10, left associativity, only parsing).
+  (at level 4, left associativity, only parsing).
 
 Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q})
-  (at level 4, x at level 10, left associativity, only parsing).
+  (at level 4, left associativity, only parsing).
 
 Notation "B + { x : A & P }"     := B + ({x:A & P})
-  (at level 4, x at level 10, left associativity, only parsing).
+  (at level 4, left associativity, only parsing).
 
 Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q})
-  (at level 4, x at level 10, left associativity, only parsing).
+  (at level 4, left associativity, only parsing).