From 9943d6b57c26b000c40feba9f31cd5a597665176 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 2 Oct 2024 17:13:44 +0200
Subject: [PATCH] fix deprecation warning

---
 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 79914865..1af4089e 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -147,7 +147,7 @@ Proof.
     match goal with H : context[_ → _ ⊢ₜ _ : _] |- _ => rename H into IH end.
     specialize (IH
       (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
-    rewrite ?map_length in IH.
+    rewrite ?length_map in IH.
     repeat rewrite fmap_app. apply IH.
     by repeat rewrite fmap_app.
   - econstructor; eauto.
@@ -155,7 +155,7 @@ Proof.
     match goal with H : context[_ → _ ⊢ₜ _ : TExist ?t] |- _ => rename t into τ end.
     specialize (IH
       (τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
-    asimpl in IH. rewrite ?map_length in IH.
+    asimpl in IH. rewrite ?length_map in IH.
     repeat rewrite fmap_app. apply IH.
     by repeat rewrite fmap_app.
 Qed.
-- 
GitLab