diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 4c30f0144da2b6d1ca799536c0937a4505c4da19..9ea8adff174f391b6f38a4a261f06e8e5901e50e 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -283,7 +283,7 @@ Section lemmas.
     - split; first done. split.
       + apply (Hm 0%nat).
       + apply equiv_dist=>n. apply Hm.
-    - split; first done. split.
+    - split; first done. intros n. split.
       + apply Hm.
       + revert n. apply equiv_dist. apply Hm.
   Qed.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index e95e32e795180d69ea7ee857e2fa1e21a2070809..5e9faf31eaab6b9842effb3d5fd63805d4721280 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -248,12 +248,12 @@ Qed.
 Lemma own_alloc_strong a (P : gname → Prop) :
   pred_infinite P →
   ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ a.
-Proof. intros HP Ha. eapply own_alloc_strong_dep with (f := λ _, a); eauto. Qed.
+Proof. intros HP Ha. eapply (own_alloc_strong_dep (λ _, a)); eauto. Qed.
 Lemma own_alloc_cofinite a (G : gset gname) :
   ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ a.
-Proof. intros Ha. eapply own_alloc_cofinite_dep with (f := λ _, a); eauto. Qed.
+Proof. intros Ha. eapply (own_alloc_cofinite_dep (λ _, a)); eauto. Qed.
 Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
-Proof. intros Ha. eapply own_alloc_dep with (f := λ _, a); eauto. Qed.
+Proof. intros Ha. eapply (own_alloc_dep (λ _, a)); eauto. Qed.
 
 (** ** Frame preserving updates *)
 Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∗ own γ a'.
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 226b4e183ce1985c7ca20207036bdb5095e89bbc..1b154fa317112762f1bbfd2d2d9901e86d08c697 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -787,7 +787,7 @@ Proof. destruct 1; inversion 1; naive_solver. Qed.
 Lemma irreducible_resolve e v1 v2 σ :
   irreducible e σ → irreducible (Resolve e (Val v1) (Val v2)) σ.
 Proof.
-  intros H κs ** [Ks e1' e2' Hfill -> step]. simpl in *.
+  intros H κs ? σ' efs [Ks e1' e2' Hfill -> step]. simpl in *.
   induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
   - subst e1'. inversion step. eapply H. by apply head_prim_step.
   - rewrite fill_app /= in Hfill.
@@ -796,6 +796,6 @@ Proof.
         (assert (to_val (fill Ks e) = Some v) as HEq by rewrite -H //);
         apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
       end).
-    apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs).
-    econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
+    eapply (H κs (fill_item _ (foldl (flip fill_item) e2' Ks)) σ' efs).
+    eapply (Ectx_step _ _ _ _ _ _ (Ks ++ [_])); last done; simpl; by rewrite fill_app.
 Qed.