Skip to content

Put `Φ` of `frame_fractional` first to make it easy to specify it if Coq fails to infer it.

Robbert Krebbers requested to merge robbert/frame_fractional_argument_order into master

This is a follow up of !928 (merged). While porting reverse dependencies we noticed that Coq is not always able to infer the Φ, see simuliris@c0dff161 for an example.

This MR makes it easier to specify the Φ, you can write apply: (frame_fractional (λ q, ...)) instead of apply: (frame_fractional _ _ _ (λ q, ...)).

Edited by Robbert Krebbers

Merge request reports