diff options
| author | herbelin | 2003-08-10 18:49:31 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-10 18:49:31 +0000 |
| commit | 779502eaf0f875821bcf2d7cbf237833dd06e07d (patch) | |
| tree | 60a7222a4dc5ff75046a902466b7b0ecc2dab024 | |
| parent | ce83183d22640b3bad592c7b65c94213a7d623f2 (diff) | |
Affichage {}+{}, niveau paire au plus haut
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4250 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Init/Notations.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 0fcb234d07..61f4daddcd 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -53,7 +53,7 @@ Uninterpreted Notation "/ x" (at level 0) (** Notations for pairs *) Uninterpreted Notation "( x , y )" (at level 0) - V8only "x , y" (at level 150, left associativity). + V8only "x , y" (at level 250, left associativity). (** Notations for sum-types *) @@ -77,7 +77,7 @@ Uninterpreted Notation "B + { x : A & P & Q }" (* At level 1 to factor with {x:A|P} etc *) -Uninterpreted Notation "{ A } + { B }" (at level 1) +Uninterpreted Notation "{ A } + { B }" (at level 1) V8only (at level 10, A at level 80). Uninterpreted Notation "A + { B }" (at level 4, left associativity) |