Skip to content

Consistent handling of pure implication and forall

Robbert Krebbers requested to merge robbert/issue127 into master

It required a bunch of additional proof mode type class instances and a hack for iSpecialize to deal with an inconsistent behavior of refine.

I hope this covers all cases.

Edited by Ralf Jung

Merge request reports