Replace most occurences of `.. || ..` by `first [..|..]`
Today I found out, as described in the Coq documentation, that the behavior of
e1 || e2 in Ltac is not what I expected. It will execute
e2 not just when
e1 fails, but also when it does not make any progress.
This problem came up when debugging an issue reported by YoungJu Song on Mattermost. He noticed that the
wp_bind tactic does not work when one tries to bind the top-level term. The code of
reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) || fail "wp_bind: cannot find" efoc "in" e
wp_bind_core is special casing the context
, and then performs just an
idtac instead of actually using the bind rule for WP.