diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 91021e1800df7e6cd0adf472658f1abab79d02f4..5035a8d3dda638c7d94efb1b4852ec8cd004923d 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -63,8 +63,6 @@ Section LiftingTests.
   Proof.
     wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
-      (* 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. *)
       ewp apply FindPred_spec; last omega.
       wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
     - by ewp apply FindPred_spec; eauto with omega.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c461fd748c5bc831a78ea12f452b26afd6a5ccbf..d1495340c3695124b68e858a6382c00c8476438f 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -190,6 +190,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
   end.
 Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
 
-(* In case the precondition does not match *)
+(* In case the precondition does not match.
+   TODO: Have one tactic unifying wp and ewp. *)
 Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
 Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).