Commit fab8ab30 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo.

parent 26dc79c4
......@@ -140,7 +140,7 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
| |- _, _ => eexists _
end;
lazymatch goal with
| |- False => fail "wp_send:" Hs' "not fresh"
| |- False => fail "wp_send:" Hs' "not found"
| _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]]
end]
| _ => fail "wp_send: not a 'wp'"
......
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