update dependencies

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") }
 ]

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.
 

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.

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 *)