Ajout 'exists! x:A, P

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 37afe09777..569662d1d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,7 +4,7 @@ Changes from V8.0
 Syntax
 
 - No more support for version 7 syntax and for translation to version 8 syntax.
-- Support for primitive interpretation of string litterals
+- Support for primitive interpretation of string literals
 - Extended support for Unicode ranges (Unicode doc TODO)
 
 Environment variables
@@ -84,9 +84,10 @@ Modules
 
 Notations
 
-- "format" option aware of recursive notations
-- added insertion of spaces by default in recursive notations w/o separators
-- no more automatic printing box in case of user-provided printing "format"
+- "format" option aware of recursive notations.
+- added insertion of spaces by default in recursive notations w/o separators.
+- no more automatic printing box in case of user-provided printing "format".
+- new notation "exists! x:A, P" for unique existence.
 
 Library
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index cefbb989de..f50e796827 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -141,6 +141,15 @@ Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
    format "'[' 'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
+Notation "'exists' ! x , P" := 
+  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
+Notation "'exists' ! x : A , P" := 
+  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
+
 
 (** Derived rules for universal quantification *)