From cd93b4853e9e5fcb3b1e1d6020382a9c1e5fd1c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 10:14:26 +0100
Subject: [PATCH] Oops, fix build.

---
 theories/program_logic/ectx_lifting.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index fbe2fd51d..165cce17f 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -67,7 +67,8 @@ Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs) "%".
-  iMod ("H" $! v2 σ2 efs with "[#]") as "(% & $ & $)"=>//; subst; auto.
+  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst.
+  by iApply big_sepL_nil.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
-- 
GitLab