Skip to content

Draft: Overlay for PR#15518

Matthieu Sozeau requested to merge mattam82/stdpp:coq-pr-15518 into master

This is an overlay for Coq PR #15518: moving apply to the evar-based unifier. This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a P <-> Q hypothesis. I think the rest is backwards compatible: mostly about using eapply in places where new existential are created, which the new apply forbids (rightfully).

Edited by Ralf Jung

Merge request reports