From 0e8c732f0532e55c78d46495f5be0fb14fad8ba1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Apr 2016 17:52:49 +0200
Subject: [PATCH] use Coq-variable-syntax

---
 heap_lang/lifting.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 07c50ce49..e3122bfd9 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -39,10 +39,7 @@ Proof.
   destruct H0 as (l & -> & ? & -> & ?).
   rewrite -(of_to_val (Loc l) (LocV l)) // in H0.
   apply of_val_inj in H0 as ->.
-  simpl. iSplitL; last done.
-  (* FIXME: I should be able to do [iSpecialize "HΦ" l]. *)
-  (* FIXME: I should be able to do [iApply "HΦ" l]. *)
-  iApply "HΦ". iSplit; done.
+  simpl. iSplitL; last done. iApply "HΦ" {l}. iSplit; done.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :
-- 
GitLab