From c2d9ad1d731cfb2699a92002d8e9be6949d006c4 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Sun, 23 Feb 2020 23:47:50 +0100
Subject: [PATCH] Fix wp_alloc when applying twp_allocN

---
 tests/heap_lang.ref            | 14 ++++++++++++++
 tests/heap_lang.v              | 14 ++++++++++++--
 theories/heap_lang/proofmode.v |  3 ++-
 3 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 075424338..ac83b6d40 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -86,6 +86,20 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  n : Z
+  H : 0 < n
+  Φ : val → iPropI Σ
+  l : loc
+  ============================
+  "HΦ" : ∀ l0 : loc, l0 ↦∗ replicate (Z.to_nat n) #0 -∗ Φ #l0
+  _ : l ↦∗ replicate (Z.to_nat n) #0
+  --------------------------------------∗
+  Φ #l
+  
 "test_array_fraction_destruct"
      : string
 1 subgoal
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 047fb65c2..8cc493fd7 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -148,13 +148,23 @@ Section tests.
   Lemma wp_alloc_array n : 0 < n →
     {{{ True }}}
       AllocN #n #0
-    {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}%I.
+    {{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}%I.
   Proof.
-    iIntros (? ?) "!> _ HΦ".
+    iIntros (? Φ) "!> _ HΦ".
     wp_alloc l as "?"; first done.
     by iApply "HΦ".
   Qed.
 
+  Lemma twp_alloc_array n : 0 < n →
+    [[{ True }]]
+      AllocN #n #0
+    [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]]%I.
+  Proof.
+    iIntros (? Φ) "!> _ HΦ".
+    wp_alloc l as "?"; first done. Show.
+    by iApply "HΦ".
+  Qed.
+
   Lemma wp_load_array l :
     {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l +ₗ #1) {{{ RET #1; True }}}.
   Proof.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 9f10d6010..2851575e3 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -484,7 +484,8 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
         first
           [reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K))
           |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-        finish ()
+        [idtac
+        |finish ()]
     in (process_single ()) || (process_array ())
   | _ => fail "wp_alloc: not a 'wp'"
   end.
-- 
GitLab