diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Logic.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 6abbfa9f87..469a9d4bf6 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -123,28 +123,28 @@ 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 (at level 200, x ident, p at level 80). + V8only "'exists' x | p" (at level 200, x ident, p at level 80). Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) : type_scope - V8only (at level 200, x ident, p at level 80). + V8only "'exists' x : t | p" (at level 200, x ident, p at level 80). 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 "'EX2' 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 80). Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) (at level 10, p, q at level 8) : type_scope - V8only "'EX2' x : t | p & q" + V8only "'exists2' x : t | p & q" (at level 200, x ident, t at level 200, p, q at level 80). -V7only [Notation All := (all ?).]. +V7only [Notation All := (all ?). Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) : type_scope V8only (at level 200, x ident, p at level 200). Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) : type_scope V8only (at level 200, x ident, t, p at level 200). - +]. (** Universal quantification *) |