diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f0170a35a0..27fcb2f295 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -292,11 +292,11 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. (** Unique existence *) -Notation "'exists' ! x , P" := (exists x', unique (fun x => P) x') +Notation "'exists' ! x , P" := (ex (unique (fun x => P))) (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. Notation "'exists' ! x : A , P" := - (exists x':A, unique (fun x:A => P) x') + (ex (unique (fun x:A => P))) (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. |