diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 12:27:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 12:27:19 +0000 |
| commit | 0541d7039eb3ac663597059413b2d9a889d6b0b5 (patch) | |
| tree | 2b58e8651d26fbc5e6590233ff3002f2dd33c262 /theories/Init/Notations.v | |
| parent | 61de148a1b0c357c54e7fecb9152c1f153552cf3 (diff) | |
Décomposition automatique des règles d'analyse syntaxique pour les
notations contenant le motif "{ _ }": permet de réperer des
incohérences de précédence comme dans "A*{B}+{C}" en présence d'une
notation "_ * { _ }" (il était parsé associant à droite au lieu de à
gauche) et de supprimer les règles spécifiques de Notations pour
parser "B+{x:A|P}" etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Notations.v')
| -rw-r--r-- | theories/Init/Notations.v | 25 |
1 files changed, 6 insertions, 19 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 356899191..92e1a818b 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -61,28 +61,15 @@ 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 *) - -(* Home-made factorization at level 4 to parse B+{x:A|P} without parentheses *) - -Reserved Notation "B + { x : A | P }" -(at level 50, x at level 99, left associativity, only parsing). - -Reserved Notation "B + { x : A | P & Q }" -(at level 50, x at level 99, left associativity, only parsing). +(** Notation "{ x }" is reserved and has a special status as component + of other notations; it is at level 0 to factor with {x:A|P} etc *) -Reserved Notation "B + { x : A & P }" -(at level 50, x at level 99, left associativity, only parsing). +Reserved Notation "{ x }" (at level 0, x at level 99). -Reserved Notation "B + { x : A & P & Q }" -(at level 50, x at level 99, left associativity, only parsing). - -(* At level 1 to factor with {x:A|P} etc *) - -Reserved Notation "{ A } + { B }" (at level 0, A at level 99). +(** Notations for sum-types *) -Reserved Notation "A + { B }" -(at level 50, B at level 99, left associativity). +Reserved Notation "{ A } + { B }" (at level 50, left associativity). +Reserved Notation "A + { B }" (at level 50, left associativity). (** Notations for sigma-types or subsets *) |