From 8a1a8f0092304f8f6facdc9498c3163fe6aacff8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 12:16:02 +0100
Subject: [PATCH] remove a now-obsolete comment

---
 heap_lang/wp_tactics.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1eb190fb3..360b44585 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
-- 
GitLab