GitLab

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.