diff options
| author | herbelin | 2006-06-09 15:43:33 +0000 |
|---|---|---|
| committer | herbelin | 2006-06-09 15:43:33 +0000 |
| commit | 2015abd3e8e4cca802d9366448fb54a0a76f8c96 (patch) | |
| tree | 138bfb9431255c60e0b02db2b80cadb805ce844c | |
| parent | 8ed6432cf793c40f69a30b1250aba7c4af31ca5f (diff) | |
Modification déf de exists! pour éviter une éta-expansion et pouvoir être filtré facilement par 'ex (unique ?P)'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8936 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |