Replace a || by 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?