From 8e787f74ca9d5b0344cd99179fe9497e300d9a0e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Aug 2023 08:25:42 +0200
Subject: [PATCH] Bump Iris (iIntros starts proof).
---
coq-actris.opam | 2 +-
theories/logrel/subtyping_rules.v | 16 ++++++++--------
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/coq-actris.opam b/coq-actris.opam
index 0c6a5cd..6a4adc2 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,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.2023-05-03.3.85295b18") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-08-03.5.fe2b6d61") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index f23854a..11b1e52 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -482,9 +482,9 @@ Section subtyping_rules.
(<!!> M) <++> S2 <:>
<!!.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
Proof.
- rewrite /LtyMsgTele. iIntros (->).
+ rewrite /LtyMsgTele. intros ->.
rewrite /lty_app /lty_message iProto_app_message /=.
- induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+ induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
- iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
- iSplit.
+ iIntros (v). iExists v.
@@ -498,9 +498,9 @@ Section subtyping_rules.
(<??> M) <++> S2 <:>
<??.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
Proof.
- rewrite /LtyMsgTele. iIntros (->).
+ rewrite /LtyMsgTele. intros ->.
rewrite /lty_app /lty_message iProto_app_message /=.
- induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+ induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
- iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
- iSplit.
+ iIntros (v). iExists v.
@@ -555,9 +555,9 @@ Section subtyping_rules.
lty_dual (<!!> M) <:>
<??.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
Proof.
- rewrite /LtyMsgTele. iIntros (->).
+ rewrite /LtyMsgTele. intros ->.
rewrite /lty_dual /lty_message iProto_dual_message /=.
- induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+ induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
- iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
- iSplit.
+ iIntros (v). iExists v.
@@ -571,9 +571,9 @@ Section subtyping_rules.
lty_dual (<??> M) <:>
<!!.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
Proof.
- rewrite /LtyMsgTele. iIntros (->).
+ rewrite /LtyMsgTele. intros ->.
rewrite /lty_dual /lty_message iProto_dual_message /=.
- induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+ induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
- iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
- iSplit.
+ iIntros (v). iExists v.
--
GitLab