diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v index 7d89fd89dc5efcb42e55c92648c5b13f5c459c39..8fef1f9255bc19dccb7235cc2886eeb52d2d412e 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