From 5062a5fc5a7c981640f870336e1d529c64afab4d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Apr 2021 16:12:38 +0200
Subject: [PATCH] remove Z.of_nat coercion entirely in std++ (but we'll add it
 in Iris for now)

---
 CHANGELOG.md       | 1 +
 theories/hashset.v | 4 ++--
 theories/prelude.v | 4 ----
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ce595d57..ebe3c7c3 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 b6d85642..72d86530 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 826a080d..9c18d5ee 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.
-- 
GitLab