From 920bc3d97b8830139045e1780f2aff4d05b910cd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Nov 2020 15:07:21 +0100
Subject: [PATCH] avoid using some auto-generated names

---
 iris/algebra/lib/gmap_view.v | 2 +-
 iris/base_logic/lib/own.v    | 6 +++---
 iris_heap_lang/lang.v        | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 4c30f0144..9ea8adff1 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 e95e32e79..5e9faf31e 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 226b4e183..1b154fa31 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.
-- 
GitLab