notes on wp failing

heap_lang/tests.v

@@ -63,7 +63,8 @@ Section LiftingTests.
   Proof.
     wp_lam>; apply later_mono; wp_op=> ?; wp_if.
     - wp_op. wp_op.
-      (* TODO: Can we use the wp tactic again here? *)
+      (* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
+         are goals being generated. That should not be the case. *)
       wp_focus (FindPred _ _). rewrite -FindPred_spec; last by omega.
       wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
     - rewrite -FindPred_spec; eauto with omega.

heap_lang/wp_tactics.v

@@ -141,7 +141,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
   end.
-Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
+Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
 
 (* In case the precondition does not match *)
 Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).