diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index a8a9b31727c01816dd6e2b0f45ef19b27edd4ebb..672c50b7739a056c979b0d350a335f1ef8a46cc7 100644
--- a/coq-iris-examples.opam
+++ b/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.2023-05-02.4.943e9b74") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index b1ff313f1fbb2c37678ebfc6c7e6f1593e3b5469..8e4a9f147a470e0dcc3e557c60891ee599b82be9 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -364,7 +364,7 @@ Section proofs.
   Proof.
     iIntros (Φ) "(Hstack & Hupd) HΦ".
     iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
-    iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first apply inner_mask_promote.
+    iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first by iApply inner_mask_promote.
     iDestruct (bi.and_mono_l _ _ (∀ (v : val) (xs : list val), _)%I with "Hupd") as "Hupd".
     { iIntros "Hupdcons". iIntros (v xs). iSpecialize ("Hupdcons" $! v xs). iApply (inner_mask_promote with "Hupdcons"). }
     iLöb as "IH".
diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v
index 85c7070ce2e885e6bd86bfd4073496c7b7b5dca2..426acc7c9fc8f4e84f179e0031f309fd4c18c71d 100644
--- a/theories/hocap/cg_bag.v
+++ b/theories/hocap/cg_bag.v
@@ -77,7 +77,7 @@ Section proof.
   Lemma bag_contents_agree γb X Y :
     bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = Y⌝.
   Proof.
-    rewrite /bag_contents. apply bi.wand_intro_r.
+    rewrite /bag_contents. apply bi.entails_wand, bi.wand_intro_r.
     rewrite -own_op own_valid uPred.discrete_valid.
     f_equiv=> /=. rewrite -pair_op.
     by intros [_ ?%to_agree_op_inv_L].
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index acf475bc311cbc71d0983a64ea7ae97b76498105..62d5f2f86db8e86f277156cd8c915d10830f6eb7 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -79,13 +79,13 @@ Qed.
 Lemma INIT_SET_RES `{saG Σ} (v: val) γ :
   INIT γ 1%Qp ==∗ SET_RES γ 1%Qp v.
 Proof.
-  apply own_update.
+  apply bi.entails_wand, own_update.
   by apply cmra_update_exclusive.
 Qed.
 Lemma SET_RES_FIN `{saG Σ} (v w: val) γ :
   SET_RES γ 1%Qp v ==∗ FIN γ w.
 Proof.
-  apply own_update.
+  apply bi.entails_wand, own_update.
   by apply cmra_update_exclusive.
 Qed.
 
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index a3ea7b8ac7084b7c999289bf072759e65520ba12..a15aee8342d245b587a7b3a72a835d3c5d39fd9d 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -60,7 +60,7 @@ Section proof.
     | _, _ => False
     end%I.
 
-  Lemma is_list_duplicate hd xs : is_list hd xs -∗ is_list hd xs ∗ is_list hd xs.
+  Lemma is_list_duplicate hd xs : is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs.
   Proof.
     iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto.
     destruct hd; last by auto.
@@ -98,7 +98,7 @@ Section proof.
   Lemma bag_contents_agree γb X Y :
     bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = Y⌝.
   Proof.
-    rewrite /bag_contents. apply bi.wand_intro_r.
+    rewrite /bag_contents. apply bi.entails_wand, bi.wand_intro_r.
     rewrite -own_op own_valid uPred.discrete_valid.
     f_equiv=> /=. rewrite -pair_op.
     by intros [_ ?%to_agree_op_inv_L].
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index dc4a5df80addf133a486b7729eda386da88f64e5..3cc02aea83c27c22cedf470d926e38c46cd802ee 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -18,7 +18,7 @@ Lemma new_pending `{oneshotG Σ} : ⊢ |==> ∃ γ, pending γ 1%Qp.
 Proof. by apply own_alloc. Qed.
 Lemma shoot `{oneshotG Σ} (v: val) γ : pending γ 1%Qp ==∗ shot γ v.
 Proof.
-  apply own_update.
+  apply bi.entails_wand, own_update.
   by apply cmra_update_exclusive.
 Qed.
 Lemma shot_not_pending `{oneshotG Σ} γ v q :
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index a8b52a1a3a7384c4e7bb239acfb87dd1348ccb49..42761fb7d3e7aa8a80ba5fd281d8bdcdc85b964c 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -530,7 +530,7 @@ Section counter_proof.
 
   (** *** Proof of [get] *)
   Lemma get_spec γs (c : val) :
-    is_counter γs c ⊢ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -568,7 +568,7 @@ Section counter_proof.
 
   (** *** Proof of [get_backup] *)
   Lemma get_backup_spec γs (c: val) :
-    is_counter γs c ⊢ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -589,7 +589,7 @@ Section counter_proof.
 
   (** *** Proof of [increment] *)
   Lemma increment_spec γs (c: val) :
-    is_counter γs c ⊢ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>.
+    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 5348b47c2aeb539b8ff4786cd4cebc9569211fe2..caee2fbcff85ff81218e065916ace6f5a98d3583 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -254,7 +254,7 @@ Lemma new_no_contra : ⊢ |==> ∃ γc, no_contra γc.
 Proof. by apply own_alloc. Qed.
 
 Lemma to_contra i1 i2 γc : no_contra γc ==∗ contra γc i1 i2.
-Proof. apply own_update. by apply cmra_update_exclusive. Qed.
+Proof. apply bi.entails_wand, own_update. by apply cmra_update_exclusive. Qed.
 
 Lemma contra_not_no_contra i1 i2 γc :
   no_contra γc -∗ contra γc i1 i2 -∗ False.
diff --git a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
index 5fa6f1852229cddbe9832a361329f61f3d1027ed..89eb137cdc9cfbb78b638b955f11add0f6a0e7f0 100644
--- a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
@@ -242,7 +242,7 @@ Section bin_log_related_under_typed_ctx.
   Proof.
     revert Γ τ Γ' τ' e e'.
     induction K as [|k K IHK]=> Γ τ Γ' τ' e e' H1 H2; simpl.
-    { inversion_clear 1; trivial. }
+    { inversion_clear 1; auto. }
     inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2].
     iIntros "#H".
     iPoseProof (IHK with "H") as "H'"; [done|done|done|].
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 929d354a8b5268c383cc6f8b0f44099aa150b1b1..21685ff166d6de23d0f3e85f056e2f1b5f93bc11 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -165,7 +165,7 @@ Section cfg.
 
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
-    apply wand_intro_r.
+    apply entails_wand, wand_intro_r.
     rewrite /heapS_mapsto -own_op own_valid uPred.discrete_valid. f_equiv.
     rewrite auth_frag_op_valid -pair_op singleton_op -pair_op.
     rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L.
@@ -180,7 +180,7 @@ Section cfg.
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
   Proof.
     rewrite /heapS_mapsto own_valid !discrete_valid auth_frag_valid.
-    by apply pure_mono=> -[_] /singleton_valid [??].
+    by apply entails_wand, pure_mono=> -[_] /singleton_valid [??].
   Qed.
   Lemma mapstoS_valid_2 l q1 q2 v1 v2 :
     l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ✓ (q1 + q2)%Qp.