From e76ca2de81eb78600dece15dd74c5eb4223f347d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Dec 2017 15:52:07 +0100
Subject: [PATCH] fix build after merging

---
 theories/heap_lang/lifting.v   |  4 ++--
 theories/heap_lang/proofmode.v | 12 ++++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 04abfc8b2..5369e0a9a 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -180,9 +180,9 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_faa E l i1 e2 i2 :
+Lemma wp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) →
-  {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ E
+  {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
   {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 31c941ec2..dac198480 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -162,16 +162,16 @@ Proof.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_faa Δ Δ' Δ'' E i K l i1 e2 i2 Φ :
+Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
   IntoVal e2 (LitV (LitInt i2)) →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ LitV (LitInt i1))%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?????; subst.
-  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ i1 _ i2).
+  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -274,10 +274,10 @@ Tactic Notation "wp_cas_suc" :=
 Tactic Notation "wp_faa" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_faa _ _ _ _ _ K); [apply _|..])
+         eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-- 
GitLab