diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:03:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:03:50 +0000 |
| commit | 7b207245cdfd7d91863441ef8e3fa4b99e830fac (patch) | |
| tree | 021ca8bb716002b55c7cbe7ef15f9f6ed493056a /theories/Init/Notations.v | |
| parent | 5eb8860b4326c61e92050a2accebf489d2ebf048 (diff) | |
Duplication temporaire des règles de syntaxe des paires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Notations.v')
| -rw-r--r-- | theories/Init/Notations.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 2a1c84165..356899191 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -51,7 +51,15 @@ Reserved Notation "x ^ y" (at level 30, right associativity). (** Notations for pairs *) -Reserved Notation "x , y" (at level 250, left associativity). +(* Temporary hack *) +Reserved Notation "( x , y )" (at level 0). +Reserved Notation "( x , y , z )" (at level 0). +Reserved Notation "( x1 , x2 , x3 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" (at level 0). (** Notations for sum-types *) |