diff options
| -rwxr-xr-x | theories7/Init/Logic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories7/Init/Logic.v b/theories7/Init/Logic.v index dc067a4b70..5881186dee 100755 --- a/theories7/Init/Logic.v +++ b/theories7/Init/Logic.v @@ -127,18 +127,18 @@ 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 99). + 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 99). + 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 99). + 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" + V8only "'exists2' x : t , p & q" (at level 200, x ident, t at level 200, p, q at level 99). V7only [Notation All := (all ?). |