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 wp_bind
contains:
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.