remove Z.of_nat coercion entirely in std++ (but we'll add it in Iris for now)

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
 

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. }

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.