Commit 8a1a8f00 authored by Ralf Jung's avatar Ralf Jung

remove a now-obsolete comment

parent 6fe4e8aa
Pipeline #165 passed with stage
......@@ -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
......
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