From df9b4add2d451c2499ca58791315f918c8158174 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 12 Dec 2021 12:58:55 -0500
Subject: [PATCH] remove a Global Arguments Pos.of_nat from the middle of a
 proof

---
 CHANGELOG.md      | 1 +
 theories/finite.v | 1 -
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36c370d0..dfd71906 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 c1a0ebc6..8ec11431 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.
-- 
GitLab