From 91a4ef45e8185aa1435f703aad88329e62647a4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Apr 2022 23:01:55 +0200
Subject: [PATCH] Bump Iris.

---
 coq-actris.opam          | 2 +-
 theories/channel/proto.v | 7 +++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/coq-actris.opam b/coq-actris.opam
index 56c6387..abd0c71 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-04-12.0.a3bed7ea") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 89eecad..e24fb86 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -878,16 +878,19 @@ Section proto.
     iApply iProto_le_exist_elim_r; iIntros (x).
     iApply "IH". iIntros (xs). iApply "H".
   Qed.
+
   Lemma iProto_le_texist_intro_l {TT : tele} (m : TT → iMsg Σ V) x :
     ⊢ (<!.. x> m x) ⊑ (<!> m x).
   Proof.
-    induction x as [|T TT x xs IH]; simpl; [iApply iProto_le_refl|].
+    induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
+    { iApply iProto_le_refl. }
     iApply iProto_le_trans; [by iApply iProto_le_exist_intro_l|]. iApply IH.
   Qed.
   Lemma iProto_le_texist_intro_r {TT : tele} (m : TT → iMsg Σ V) x :
     ⊢ (<?> m x) ⊑ (<?.. x> m x).
   Proof.
-    induction x as [|T TT x xs IH]; simpl; [iApply iProto_le_refl|].
+    induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
+    { iApply iProto_le_refl. }
     iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
   Qed.
 
-- 
GitLab