From 6b124185832b13e73a06ee6c28a37a096ffabe04 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 09:39:33 +0200
Subject: [PATCH] Forwards compatibility fix for
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555
---
theories/logrel/F_mu_ref_conc/typing.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index c6af41f7..abe7e7f5 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -113,8 +113,8 @@ Proof.
- rename select (_ !! _ = Some _) into H.
apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
- f_equal. eauto.
- - f_equal. rewrite ->map_length in *. done.
- - rewrite ->map_length in *; by f_equal.
+ - f_equal. rewrite ->fmap_length in *. done.
+ - rewrite ->fmap_length in *; by f_equal.
Qed.
(** Weakening *)
--
GitLab