diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1eb190fb3bb218a635b6e1158e32673d84041ce7..360b44585ac08e5ad082818e6561f2d518c01fa5 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -3,8 +3,6 @@ From heap_lang Require Export tactics substitution.
 Import uPred.
 
 (** wp-specific helper tactics *)
-(* First try to productively strip off laters; if that fails, at least
-   cosmetically get rid of laters in the conclusion. *)
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac