diff options
author | 2004-02-12 12:27:19 +0000 | |
---|---|---|
committer | 2004-02-12 12:27:19 +0000 | |
commit | 0541d7039eb3ac663597059413b2d9a889d6b0b5 (patch) | |
tree | 2b58e8651d26fbc5e6590233ff3002f2dd33c262 /theories7 | |
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 'theories7')
-rw-r--r-- | theories7/Init/Notations.v | 30 | ||||
-rwxr-xr-x | theories7/Init/Specif.v | 11 |
2 files changed, 8 insertions, 33 deletions
diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v index 3cdb8e6ce..2e9e1692d 100644 --- a/theories7/Init/Notations.v +++ b/theories7/Init/Notations.v @@ -69,33 +69,19 @@ Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0). Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0). Uninterpreted V8Notation "( 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 *) - -Uninterpreted Notation "B + { x : A | P }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). - -Uninterpreted Notation "B + { x : A | P & Q }" - (at level 4, left associativity, only parsing) - V8only (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 1 to factor with {x:A|P} etc *) -Uninterpreted Notation "B + { x : A & P }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). - -Uninterpreted Notation "B + { x : A & P & Q }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). +Uninterpreted Notation "{ x }" (at level 1) + V8only (at level 0, x at level 99). -(* At level 1 to factor with {x:A|P} etc *) +(** Notations for sum-types *) -Uninterpreted Notation "{ A } + { B }" (at level 1) - V8only (at level 0, A at level 99). +Uninterpreted Notation "{ A } + { B }" (at level 4, left associativity) + V8only (at level 50, left associativity). Uninterpreted Notation "A + { B }" (at level 4, left associativity) - V8only (at level 50, B at level 99, left associativity). + V8only (at level 50, left associativity). (** Notations for sigma-types or subsets *) diff --git a/theories7/Init/Specif.v b/theories7/Init/Specif.v index 2e49fab04..1255a5a28 100755 --- a/theories7/Init/Specif.v +++ b/theories7/Init/Specif.v @@ -108,17 +108,6 @@ Inductive sumor [A:Set;B:Prop] : Set where "A + { B }" := (sumor A B) : type_scope. -(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) - -Notation "B + { x : A | P }" := B + (sig A [x:A]P) - (only parsing) : type_scope. -Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) - (only parsing) : type_scope. -Notation "B + { x : A & P }" := B + (sigS A [x:A]P) - (only parsing) : type_scope. -Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) - (only parsing) : type_scope. - (** Choice *) Section Choice_lemmas. |