diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Logic.v | 8 | ||||
| -rw-r--r-- | theories/Init/LogicSyntax.v | 8 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 48 |
3 files changed, 32 insertions, 32 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 680b1e20e..4c284818b 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -126,19 +126,19 @@ Definition all := [A:Type][P:A->Prop](x:A)(P x). V7only [ Notation Ex := (ex ?). ]. Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) : type_scope - V8only "'exists' x | p" (at level 200, x ident, p at level 80). + V8only "'exists' x | p" (at level 200, x ident, p at level 99). Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) : type_scope - V8only "'exists' x : t | p" (at level 200, x ident, p at level 80). + V8only "'exists' x : t | p" (at level 200, x ident, p at level 99). V7only [ Notation Ex2 := (ex2 ?). ]. Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) : type_scope - V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 80). + V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 99). Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) (at level 10, p, q at level 8) : type_scope V8only "'exists2' x : t | p & q" - (at level 200, x ident, t at level 200, p, q at level 80). + (at level 200, x ident, t at level 200, p, q at level 99). V7only [Notation All := (all ?). Notation "'ALL' x | p" := (all ? [x]p) diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 102e67db6..f95f56d37 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -24,17 +24,17 @@ Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) V7only [ Notation Ex := (ex ?). ]. Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) - V8only "'exists' x , p" (at level 200, x at level 80). + V8only "'exists' x , p" (at level 200, x at level 99). Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) - V8only "'exists' x : t , p" (at level 200, x at level 80). + V8only "'exists' x : t , p" (at level 200, x at level 99). V7only [ Notation Ex2 := (ex2 ?). ]. Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) - V8only "'exists2' x , p & q" (at level 200, x at level 80). + V8only "'exists2' x , p & q" (at level 200, x at level 99). Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) (at level 10, p, q at level 8) - V8only "'exists2' x : t , p & q" (at level 200, x at level 80). + V8only "'exists2' x : t , p & q" (at level 200, x at level 99). V7only[ (** Parsing only of things in [Logic.v] *) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 8a107f5c0..149c75751 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -18,7 +18,7 @@ Uninterpreted Notation "x \/ y" (at level 7, right associativity). Uninterpreted Notation "x <-> y" (at level 8, right associativity). Uninterpreted Notation "~ x" (at level 5, right associativity) - V8only (at level 55, right associativity). + V8only (at level 75, right associativity). (** Notations for equality and inequalities *) @@ -34,28 +34,28 @@ Uninterpreted Notation "x <> y :> T" Uninterpreted Notation "x <> y" (at level 5, no associativity). -Uninterpreted V8Notation "x <= y" (at level 50, no associativity). -Uninterpreted V8Notation "x < y" (at level 50, no associativity). -Uninterpreted V8Notation "x >= y" (at level 50, no associativity). -Uninterpreted V8Notation "x > y" (at level 50, no associativity). +Uninterpreted V8Notation "x <= y" (at level 70, no associativity). +Uninterpreted V8Notation "x < y" (at level 70, no associativity). +Uninterpreted V8Notation "x >= y" (at level 70, no associativity). +Uninterpreted V8Notation "x > y" (at level 70, no associativity). -Uninterpreted V8Notation "x <= y <= z" (at level 50, y at next level). -Uninterpreted V8Notation "x <= y < z" (at level 50, y at next level). -Uninterpreted V8Notation "x < y < z" (at level 50, y at next level). -Uninterpreted V8Notation "x < y <= z" (at level 50, y at next level). +Uninterpreted V8Notation "x <= y <= z" (at level 70, y at next level). +Uninterpreted V8Notation "x <= y < z" (at level 70, y at next level). +Uninterpreted V8Notation "x < y < z" (at level 70, y at next level). +Uninterpreted V8Notation "x < y <= z" (at level 70, y at next level). (** Arithmetical notations (also used for type constructors) *) Uninterpreted Notation "x * y" (at level 3, right associativity) - V8only (at level 30, left associativity). -Uninterpreted V8Notation "x / y" (at level 30, left associativity). + V8only (at level 40, left associativity). +Uninterpreted V8Notation "x / y" (at level 40, left associativity). Uninterpreted Notation "x + y" (at level 4, left associativity). Uninterpreted Notation "x - y" (at level 4, left associativity). -Uninterpreted Notation "- x" (at level 0) V8only (at level 40). +Uninterpreted Notation "- x" (at level 0) V8only (at level 50). Uninterpreted Notation "/ x" (at level 0) - V8only (at level 30, left associativity). + V8only (at level 40, left associativity). -Uninterpreted V8Notation "x ^ y" (at level 20, left associativity). +Uninterpreted V8Notation "x ^ y" (at level 30, left associativity). (** Notations for pairs *) @@ -68,38 +68,38 @@ Uninterpreted Notation "( x , y )" (at level 0) Uninterpreted Notation "B + { x : A | P }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, 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 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). Uninterpreted Notation "B + { x : A & P }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, 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 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). (* At level 1 to factor with {x:A|P} etc *) Uninterpreted Notation "{ A } + { B }" (at level 1) - V8only (at level 0, A at level 80). + V8only (at level 0, A at level 99). Uninterpreted Notation "A + { B }" (at level 4, left associativity) - V8only (at level 40, B at level 80, left associativity). + V8only (at level 50, B at level 99, left associativity). (** Notations for sigma-types or subsets *) Uninterpreted Notation "{ x : A | P }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A | P & Q }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A & P }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A & P & Q }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Delimits Scope type_scope with T. |