Renaming in rules.v

theories/logrel/rules.v

@@ -271,22 +271,21 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v' t τ
+  Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v t τ
     (Hmasked : nclose specN ⊆ E1) :
-    l ↦ₛ{q} v' -∗
-    (l ↦ₛ{q} v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v') : τ)
-    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Load (# l)) : τ.
+    l ↦ₛ{q} v -∗
+    (l ↦ₛ{q} v -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v) : τ)
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ (fill K !#l) : τ.
   Proof.
     iIntros "Hl Hlog".
-    pose (Φ := (fun w => ⌜w = v'⌝ ∗ l ↦ₛ{q} v')%I).
+    pose (Φ := (fun w => ⌜w = v⌝ ∗ l ↦ₛ{q} v)%I).
     iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=". iExists v'.
+      iIntros (ρ j K') "#Hs Hj /=". iExists v.
       tp_load j.
       iFrame. eauto. }
-    iIntros (v) "[% Hl]"; subst.
-    iApply "Hlog".
-    done.
+    iIntros (?) "[% Hl]"; subst.
+    by iApply "Hlog".
   Qed.
 
   Lemma bin_log_related_store_r Δ Γ E1 E2 K l e e' v v' τ
@@ -603,14 +602,14 @@ Section properties.
     iApply (wp_load with "Hl"); auto.
   Qed.
 
-  Lemma bin_log_related_load_l' Δ Γ E1 K l q v' t τ :
-    ▷ l ↦ᵢ{q} v' -∗
-    ▷ (l ↦ᵢ{q} v' -∗ ({E1;Δ;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ))
+  Lemma bin_log_related_load_l' Δ Γ E1 K l q v t τ :
+    ▷ l ↦ᵢ{q} v -∗
+    ▷ (l ↦ᵢ{q} v -∗ ({E1;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ))
     -∗ {E1;Δ;Γ} ⊨ fill K !#l ≤log≤ t : τ.
   Proof.
     iIntros "Hl Hlog".
     iApply (bin_log_related_load_l); auto.
-    iExists v'.
+    iExists v.
     iModIntro.
     by iFrame.
   Qed.