WP tactics do not `simpl` enough
See for example line 133 of ticket_lock.v, after calling wp_cas_fail:
|={⊤ ∖ ↑N,⊤}=> WP if: LitV false then (wait_loop #n) (#lo, #ln) else acquire (#lo, #ln) {{ v, ϕ v }}Here, there is an of_val (LitV false), which should be simplified into Lit false, which is then pretty printed properly.
I expect the problem to be related to the fact that the WP in this case is below an update modality, and as such, simpl is not used.