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).