Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict with FSets

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

1 files changed, 4 insertions, 3 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 53a526895..f0170a35a 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -285,17 +285,18 @@ Hint Immediate sym_eq sym_not_eq: core v62.
 Definition subrelation (A B : Type) (R R' : A->B->Prop) :=
   forall x y, R x y -> R' x y.
 
-Definition singleton (A : Type) (P : A->Prop) (x:A) :=
+Definition unique (A : Type) (P : A->Prop) (x:A) :=
   P x /\ forall (x':A), P x' -> x=x'.
 
 Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
 
 (** Unique existence *)
 
-Notation "'exists' ! x , P" := (exists x', singleton (fun x => P) x')
+Notation "'exists' ! x , P" := (exists x', unique (fun x => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" := (exists x':A, singleton (fun x:A => P) x')
+Notation "'exists' ! x : A , P" := 
+  (exists x':A, unique (fun x:A => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.