From f3dc121d0270657452c603dc66274cfc9aeb143e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 May 2021 13:32:07 +0200
Subject: [PATCH] update dependencies

---
 opam                              |  2 +-
 theories/channel/proto.v          |  4 ++--
 theories/examples/swap_mapper.v   | 12 ++++++------
 theories/logrel/subtyping_rules.v |  8 ++++----
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/opam b/opam
index 52a3406..fc9bcb0 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-04-20.0.7a260d80") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-05-27.2.59e3a162") | (= "dev") }
 ]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f7008ba..2c91fda 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1287,9 +1287,9 @@ Section proto.
   Qed.
 
   Global Instance iProto_le_from_modal a v p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
-  Proof. apply iProto_le_base. Qed.
+  Proof. intros _. apply iProto_le_base. Qed.
 
 End proto.
 
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index cbb3df7..22adfcd 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -71,9 +71,9 @@ Section with_Σ.
   Qed.
 
   Global Instance send_once_from_modal p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (∀ x, p1 x ⊑ p2 x)
+    FromModal True (modality_instances.modality_laterN 1) (∀ x, p1 x ⊑ p2 x)
               ((send_once p1) ⊑ (send_once p2)) (∀ x, p1 x ⊑ p2 x).
-  Proof. apply send_once_mono. Qed.
+  Proof. intros _. apply send_once_mono. Qed.
 
   Lemma recv_once_mono prot1 prot2 x :
     ▷ (prot1 ⊑ prot2) -∗ recv_once prot1 x ⊑ recv_once prot2 x.
@@ -84,18 +84,18 @@ Section with_Σ.
   Qed.
 
   Global Instance recv_once_from_modal p1 p2 x :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((recv_once p1 x) ⊑ (recv_once p2 x)) (p1 ⊑ p2).
-  Proof. apply recv_once_mono. Qed.
+  Proof. intros _. apply recv_once_mono. Qed.
 
   Lemma map_once_mono prot1 prot2 :
     ▷ (prot1 ⊑ prot2) -∗ map_once prot1 ⊑ map_once prot2.
   Proof. iIntros "Hsub". iModIntro. iIntros (x). iModIntro. eauto. Qed.
 
   Global Instance map_once_from_modal p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((map_once p1) ⊑ (map_once p2)) (p1 ⊑ p2).
-  Proof. apply map_once_mono. Qed.
+  Proof. intros _. apply map_once_mono. Qed.
 
   Definition mapper_prot_once :=
     (map_once mapper_prot)%proto.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 081681e..d87b685 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -450,17 +450,17 @@ Section subtyping_rules.
   Qed.
 
   Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
               ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
   Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_send. iApply lty_le_refl. done.
   Qed.
 
   Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
               ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
   Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_recv. iApply lty_le_refl. done.
   Qed.
 
   (** Algebraic laws *)
-- 
GitLab