update dependencies

coq-iris-examples.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-07-27.1.d01b4bc8") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/barrier/example_client.v

@@ -62,7 +62,7 @@ Section ClosedProofs.
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
 
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy Σ)=> ??. iIntros "_". iApply client_safe. Qed.
+Proof. apply (heap_adequacy Σ)=>?. iIntros "_". iApply client_safe. Qed.
 
 End ClosedProofs.
 

theories/logatom/elimination_stack/stack.v

@@ -23,7 +23,7 @@ Global Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
 Proof. solve_inG. Qed.
 
 Section stack.
-  Context `{!heapGS Σ, stackG Σ} {aheap: atomic_heap Σ} (N : namespace).
+  Context `{!heapGS Σ, !stackG Σ, !atomic_heap} (N : namespace).
   Notation iProp := (iProp Σ).
 
   Let offerN := N .@ "offer".
@@ -363,7 +363,7 @@ Section stack.
 
 End stack.
 
-Definition elimination_stack `{!heapGS Σ, stackG Σ} {aheap: atomic_heap Σ} :
+Definition elimination_stack `{!heapGS Σ, !stackG Σ, !atomic_heap} :
   atomic_stack Σ :=
   {| spec.new_stack_spec := new_stack_spec;
      spec.push_spec := push_spec;

theories/logrel/F_mu_ref_conc/binary/soundness.v

@@ -20,7 +20,7 @@ Proof.
   intros Hlog Hsteps.
   cut (adequate NotStuck e ∅ (λ _ _, ∃ thp' h v, rtc erased_step ([e'], ∅) (of_val v :: thp', h))).
   { destruct 1; naive_solver. }
-  eapply (wp_adequacy_lc Σ _); iIntros (Hinv ??).
+  eapply (wp_adequacy Σ _); iIntros (Hinv ?).
   iMod (gen_heap_init (∅: state)) as (Hheap) "[Hh _]".
   iMod (own_alloc (● (to_tpool [e'], ∅)
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".

theories/logrel/F_mu_ref_conc/unary/soundness.v

@@ -16,7 +16,7 @@ Proof.
   intros Hlog ??.
   cut (adequate NotStuck e σ (λ _ _, True));
     first by intros [_ Hsafe]; eapply Hsafe; eauto.
-  eapply (wp_adequacy_lc Σ _). iIntros (Hinv ??).
+  eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iMod (gen_heap_init σ) as (Hheap) "[Hh _]".
   iModIntro. iExists (λ σ _, gen_heap_interp σ), (λ _, True%I); iFrame.
   set (HeapΣ := (HeapIG Σ Hinv Hheap)).

theories/logrel/stlc/soundness.v

@@ -16,8 +16,8 @@ Proof.
   set (Σ := invΣ). intros.
   cut (adequate NotStuck e () (λ _ _, True));
     first by intros [_ Hsafe]; eapply Hsafe; eauto.
-  eapply (wp_adequacy_lc Σ _). iIntros (Hinv ??).
+  eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//.
-  set (HΣ := IrisG _ _ Hinv (λ _ _ _ _, True)%I (λ _, True)%I).
+  set (HΣ := IrisG Hinv (λ _ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"); first by iApply wp_soundness. eauto.
 Qed.