diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 773fd83a1a6ed09eb55e47646fdddb56619abe4d..892bbd87c6b359f2e5125708f7ffaed5ac3ed9bd 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 b7a654e70487dc504fc30c8617e07e095bc93400..72fe38524145498be9557a834da6711fb9547074 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 cba58c5b63671aba8812fcdb1c0d327c91467b78..790f4d3c51cf15ea59d7655e1dc31dd1049ec00a 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.