From 2015abd3e8e4cca802d9366448fb54a0a76f8c96 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jun 2006 15:43:33 +0000
Subject: 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
---
 theories/Init/Logic.v | 4 ++--
 1 file 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.
 
-- 
cgit v1.2.3