Commit db3512f7 authored by Robbert Krebbers's avatar Robbert Krebbers

Add comment to wp_done and slightly simplify it.

parent 6545516e
Pipeline #2282 passed with stage
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment