diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rwxr-xr-x | theories/Init/Logic.v | 8 |
1 files changed, 4 insertions, 4 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) |