Merged requested to merge ralf/wp-bind-empty into master
first [ .. ] to avoid the implicit
progress on the LHS of
There are quite a few other
|| left in this file; I did not audit them, but this one stood out:
Ltac wp_value_head := first [eapply tac_wp_value || eapply tac_twp_value].
That's probably a typo?