diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 075424338a0ad49e124b52b9c1d02a07def0b5d0..ac83b6d40d0301db200c115e332c6793333cf286 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 047fb65c2694feea51bdfd484ac546a27feb164d..8cc493fd75bb55ba835d2c7b1f1f2ab639793578 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 9f10d6010e614e7d6f3cad50b9ee09262a581a38..2851575e316f241e211dd63dde579bfc62b41d47 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.