Skip to content

fix wp_bind with empty context

Ralf Jung requested to merge ralf/wp-bind-empty into master

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?

Merge request reports