From b39e580751dd3a87fae92b254408d59d864a89ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Feb 2025 09:21:31 +0100
Subject: [PATCH] Forward compatibility patch for
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555
---
theories/examples/stack_helping/helping_wrapper.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 7684d7d..acb7334 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -161,8 +161,7 @@ Section offerReg_rules.
symmetry. apply agree_included.
by apply to_agree_included.
+ rewrite lookup_singleton_ne; eauto.
- destruct ((offerize <$> N !! i)) as [?|] eqn:He;
- rewrite He; simpl; done. }
+ by case: ((offerize <$> N !! i)). }
by rewrite Hfoo.
Qed.
--
GitLab