From 01d2e142ced142f21d2b477710564a25beac3525 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 May 2020 18:26:55 +0200
Subject: [PATCH] review feedback

---
 theories/heap_lang/derived_laws.v   | 11 +++++------
 theories/heap_lang/primitive_laws.v |  3 ++-
 theories/program_logic/lifting.v    |  3 +++
 3 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/theories/heap_lang/derived_laws.v b/theories/heap_lang/derived_laws.v
index 704c18a8e..1e36d1f7a 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/theories/heap_lang/derived_laws.v
@@ -1,13 +1,12 @@
-(** This file extens the HeapLang program logic with some derived laws about
-arrays and prophecies.
+(** This file extends the HeapLang program logic with some derived laws (not
+using the lifting lemmas) about arrays and prophecies.
 
-For more array operations, see [heap_lang.lib.array].
-*)
+For utility functions on arrays (e.g., freeing/copying an array), see
+[heap_lang.lib.array].  *)
 
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
@@ -333,7 +332,7 @@ Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
   {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
 Proof.
   iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
-  iApply wp_pure_step_later=> //=. iApply wp_value.
+  iApply lifting.wp_pure_step_later=> //=. iApply wp_value.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 9fc1766cf..047c26815 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -1,4 +1,5 @@
-(** This file proves the basic laws of the HeapLang program logic. *)
+(** This file proves the basic laws of the HeapLang program logic by applying
+the Iris lifting lemmas. *)
 
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 96118502d..d7e657de4 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,3 +1,6 @@
+(** The "lifting lemmas" in this file serve to lift the rules of the operational
+semantics to the program logic. *)
+
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
-- 
GitLab