Merge branch 'fix-twp_allocN-tac' into 'master'

Fix wp_alloc when applying twp_allocN

See merge request iris/iris!382

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

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.

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.