From 781d0b1e3d0e7b0a8f29ea26903a61c6dbb0861a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 12:44:25 -0400
Subject: [PATCH] avoid a whacky rewrite that no longer works with Coq 8.16

---
 theories/typing/function.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7de88219..b374b1ce 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -357,7 +357,7 @@ Section typing.
     ⊢ typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HL HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
+    iApply typed_body_mono; [| |done|by iApply type_call']; simpl.
     - etrans.
       + eapply (incl_cctx_incl _ [_]); by intros ? ->%elem_of_list_singleton.
       + apply cctx_incl_cons; first done. intros args. by inv_vec args.
-- 
GitLab