From db3512f79c06cacf9460185127670f3e9b12b646 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jul 2016 17:53:01 +0200
Subject: [PATCH] Add comment to wp_done and slightly simplify it.

---
 heap_lang/wp_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 7d89fd89d..8fef1f925 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,7 +9,7 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-(* TODO: Do something better here *)
+(* Solves side-conditions generated by the wp tactics *)
 Ltac wp_done :=
   match goal with
   | |- Closed _ _ => solve_closed
-- 
GitLab