Skip to content

do not make use of wp_bind_inv unnecessarily

Ralf Jung requested to merge ralf/wp_bind_inv into master

@janno asked for this when porting iGPS to PureExec. iGPS does not currently have wp_bind_inv, and it is not clear whether we can make that law hold.

The new ltac in wp_pure is horrible, I hope @robbertkrebbers can find a better way. :) Ideally, we can make use of the fact that pure_exec_ctx is an instance. If not, it should probably be downgraded to a lemma.

Merge request reports