Draft: Overlay for PR#15518
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).