The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
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" ewp_bind_core is special casing the context [], and then performs just an idtac instead of actually using the bind rule for WP.