diff --git a/theories/ZornsLemma/DirectedSets.v b/theories/ZornsLemma/DirectedSets.v
index 2b31139e..6630a3cb 100644
--- a/theories/ZornsLemma/DirectedSets.v
+++ b/theories/ZornsLemma/DirectedSets.v
@@ -105,11 +105,11 @@ Arguments not_eventually_eal_not {I}.
 
 Notation "'for' 'large' i : I , p" :=
   (eventually (fun i:I => p))
-  (at level 200, i ident, right associativity).
+  (at level 200, i name, right associativity).
 
 Notation "'exists' 'arbitrarily' 'large' i : I , p" :=
   (exists_arbitrarily_large (fun i:I => p))
-  (at level 200, i ident, right associativity).
+  (at level 200, i name, right associativity).
 
 Section nat_DS.
 
diff --git a/theories/ZornsLemma/EnsemblesSpec.v b/theories/ZornsLemma/EnsemblesSpec.v
index 53017bdd..3de73bff 100644
--- a/theories/ZornsLemma/EnsemblesSpec.v
+++ b/theories/ZornsLemma/EnsemblesSpec.v
@@ -10,7 +10,7 @@ Definition characteristic_function_to_ensemble {X:Type} (P:X->Prop) : Ensemble X
 
 Notation "[ x : X | P ]" :=
   (characteristic_function_to_ensemble (fun x:X => P))
-  (x ident).
+  (x name).
 
 Lemma characteristic_function_to_ensemble_is_identity:
   forall {X:Type} (P:X->Prop),
diff --git a/theories/ZornsLemma/EnsemblesUtf8.v b/theories/ZornsLemma/EnsemblesUtf8.v
index 452a8436..305c6292 100644
--- a/theories/ZornsLemma/EnsemblesUtf8.v
+++ b/theories/ZornsLemma/EnsemblesUtf8.v
@@ -30,15 +30,15 @@ Notation "∅" := Empty_set (at level 0).
 
 Notation "⋃ F" := (FamilyUnion F) (at level 0).
 Notation "⋃ [ x : X ] S" :=
-  (IndexedUnion (fun x:X => S)) (at level 0, x ident).
+  (IndexedUnion (fun x:X => S)) (at level 0, x name).
 Notation "\\// [ x : X ] S" :=
-  (IndexedUnion (fun x:X => S)) (only parsing, x ident, at level 0).
+  (IndexedUnion (fun x:X => S)) (only parsing, x name, at level 0).
 Notation "⋂ F" := (FamilyIntersection F) (at level 0).
 Notation "⋂ [ x : X ] S" :=
-  (IndexedIntersection (fun x:X => S)) (at level 0, x ident).
+  (IndexedIntersection (fun x:X => S)) (at level 0, x name).
 Notation "//\\ [ x : X ] S" :=
   (IndexedIntersection (fun x:X => S))
-  (only parsing, x ident, at level 0).
+  (only parsing, x name, at level 0).
 
 (* test *)
 (*