From bfca791ecb02cb381d08b5bb6b7a3cf31ecb549e Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Thu, 11 Feb 2021 09:40:52 -0600
Subject: [PATCH] Avoid relying on buggy simpl never behavior

Alternate take on
https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e,
which is used as an overlay in Coq for
https://github.com/coq/coq/pull/13448.
---
 theories/finite.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/finite.v b/theories/finite.v
index 6bd7d4af..14a81f14 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -64,8 +64,8 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
   intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
-  rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
-  apply list_find_Some in Hi; naive_solver.
+  rewrite Hi; unfold decode_nat, decode; simpl. rewrite !Nat2Pos.id by done.
+  simpl. apply list_find_Some in Hi; naive_solver.
 Qed.
 
 Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
-- 
GitLab