From 82bd9f1dd2643d577c2570a6bc03b11eb72e6604 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 2 Jun 2021 20:46:58 +0200
Subject: [PATCH] fix for std++ update

---
 iris/program_logic/language.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 280a6d36b..547c9c53a 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -198,7 +198,7 @@ Section language.
   Proof.
     intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
     move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
-    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
+    intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
     exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.
-- 
GitLab