diff --git a/CHANGELOG.md b/CHANGELOG.md
index ce595d577fa1ba894d48f6d51fb21c1399159f95..ebe3c7c355e84296b21d279e735f78b39b5f358f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ API-breaking change is listed.
   + Add lemmas for `∈` and `∉` specific for multisets, since the set lemmas no
     longer work for multisets.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
+- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
 
 ## std++ 1.5.0
 
diff --git a/theories/hashset.v b/theories/hashset.v
index b6d8564229720bedd7f58a9b8ead956a07b1e1d4..72d865301af8f094832ef5b41a817c57dd3aff95 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -126,7 +126,7 @@ Definition remove_dups_fast (l : list A) : list A :=
   | [] => []
   | [x] => [x]
   | _ =>
-     let n : Z := length l in
+     let n : Z := Z.of_nat (length l) in
      elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
        hashset (λ x, hash x `mod` (2 * n))%Z)
   end.
@@ -134,7 +134,7 @@ Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
 Proof.
   destruct l as [|x1 [|x2 l]]; try reflexivity.
   unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
-  generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
+  generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f.
   rewrite elem_of_elements; split.
   - revert x. induction l as [|y l IH]; intros x; simpl.
     { by rewrite elem_of_empty. }
diff --git a/theories/prelude.v b/theories/prelude.v
index 826a080d9f4596871bea284db0b4f4d05561b8de..9c18d5eef37d92341f80527275841733a676c2b2 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -13,7 +13,3 @@ From stdpp Require Export
   list_numbers
   lexico.
 From stdpp Require Import options.
-
-(** We are phasing out this coercion inside std++, but currently
-keep it enabled for users to ensure backwards compatibility. *)
-Coercion Z.of_nat : nat >-> Z.