From 148867183346b43bc6546c7cebf3f9d11b480ffe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Oct 2023 14:45:02 +0200
Subject: [PATCH] Fixes for Coq 8.18.

---
 theories/examples/stack_helping/helping_wrapper.v | 2 +-
 theories/examples/stack_helping/stack.v           | 2 +-
 theories/logic/spec_ra.v                          | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 773fd83..892bbd8 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -74,7 +74,7 @@ Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
 
 Lemma to_offer_reg_valid N : ✓ to_offer_reg N.
 Proof.
-  intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
+  intros l. rewrite lookup_fmap. case: (N !! l); simpl; try done.
   intros [[v γ] k]; simpl. done.
 Qed.
 
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index b7a654e..72fe385 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -100,7 +100,7 @@ Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
 
 Lemma to_offer_reg_valid N : ✓ to_offer_reg N.
 Proof.
-  intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
+  intros l. rewrite lookup_fmap. case: (N !! l); simpl; try done.
   intros [[v γ] k]; simpl. done.
 Qed.
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index cba58c5..790f4d3 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -144,7 +144,7 @@ Section to_heap.
   Qed.
 
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
+  Proof. intros l. rewrite lookup_fmap. by case: (σ !! l). Qed.
 
 End to_heap.
 
-- 
GitLab