Remove all uses of legacy `apply` in Proof Mode (!1077) · Merge requests · Iris / Iris

Robbert Krebbers requested to merge robbert/resolve_tc into master Sep 23, 2024

This MR makes use of https://github.com/coq/coq/pull/13071, which is new in Coq 8.19. So Coq 8.18 can no longer be supported. Since we have the policy of supporting the last two Coq versions that would be OK.

This MR might make it possible for the Coq devs to fix https://github.com/coq/coq/issues/6583, a bug which we accidentally used as a "feature".

It would be interesting to see timing and impact on reverse dependencies.

Remove all uses of legacy `apply` in Proof Mode

Merge request reports