diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36c370d031dbaedddf52369d6400edaab0a1aab9..dfd7190618e803197fcbbbc2f7f13f4417b96cbf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,7 @@ Coq 8.10 is no longer supported by this release.
 - Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
 - Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
+- Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/theories/finite.v b/theories/finite.v
index c1a0ebc65d58ecfa408324f2e77392aba329e816..8ec114313a2f979ee97d250791ccaed48ae37a37 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -19,7 +19,6 @@ Program Definition finite_countable `{Finite A} : Countable A := {|
     Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
-Global Arguments Pos.of_nat : simpl never.
 Next Obligation.
   intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
   destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.