diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:29:30 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 15:29:30 +0000 |
| commit | 000b7a6dbbc1399d04e514aa7f515894b1652e54 (patch) | |
| tree | 4c781d6d7a49b951fc1cbc4b983dd883dbc4a3e8 /theories7 | |
| parent | 7b207245cdfd7d91863441ef8e3fa4b99e830fac (diff) | |
exists | --> exists ,
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7')
| -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 dc067a4b7..5881186de 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 ?). |