From 4a6e41945e6098a9fa673dab7c57c293ed98c127 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Feb 2025 09:45:38 +0100
Subject: [PATCH] Forward compatibility fixes for
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555

---
 theories/simulang/logical_heap.v | 2 +-
 theories/stacked_borrows/type.v  | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/simulang/logical_heap.v b/theories/simulang/logical_heap.v
index 44bd5ba2..4f5a9f8d 100644
--- a/theories/simulang/logical_heap.v
+++ b/theories/simulang/logical_heap.v
@@ -113,7 +113,7 @@ Section to_heap.
   Implicit Types σ : gmap loc (lock_state * val).
 
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+  Proof. intros l. rewrite lookup_fmap. case: (σ !! l)=> [[[|n] v]|] //=. Qed.
 
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
diff --git a/theories/stacked_borrows/type.v b/theories/stacked_borrows/type.v
index 23bec750..af143722 100644
--- a/theories/stacked_borrows/type.v
+++ b/theories/stacked_borrows/type.v
@@ -263,10 +263,10 @@ Proof.
      | GenNode 5 Ts => Sum (go <$> Ts)
      | _ => FixedSize 0
      end) _).
-  fix FIX 1. intros [| | |Ts|Ts|Ts]; f_equal=>//; revert Ts; clear -FIX.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
+  fix FIX 1. intros [| | |Ts|Ts|Ts]; csimpl; f_equal=>//; revert Ts; clear -FIX.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
 Qed.
 
 (** Finding sum types *)
-- 
GitLab