Use `notypeclasses refine` in `iPoseProof*` helpers for `iDestruct`.
This MR ensures compatiblity with https://github.com/coq/coq/pull/10762 by using
notypeclasses refine for the following:
- Applying the various helper lemmas for
- The base case of
iAssumption, i.e. it now uses a
from_assumption_exact : FromAssumption p P P. This also affects the unification with premises in
In addition, I have rewritten
iIntoEmpValid to use a series of lemmas in a
notypeclasses refine loops instead of the old fragile Ltac code. The advantage is that matching now happens up to unification, and we no longer need the
hnf hacks that were present in this code.
An advantage of using
notypeclasses refine in these pieces of code is that type class search is no longer triggered randomly. It basically avoids to https://github.com/coq/coq/issues/6583. Another advantage is that we now use the new unification algorithm in more places, which is often better behaved.
A disadvantage is that this MR breaks some code. Naturally, since type search search is no longer called randomly (it is basically delayed until the end of the
iPoseProof), unification is often presented with more complicated goals because fewer TC arguments are resolved (over eagerly). As such, some proof mode tactics that used to succeed, will now fail. By using the new unification algorithm for
iAssumption (item 2, above), I managed to reduce the number of cases where this problem appeared. However, some tactics will of course behave differently because the new unification algorithm is used.
Although breakage is inevitable, the number of changes to the reverse dependencies are limited: Rustbelt (2 lines changed), gpfls (12 lines changed), Rustbelt-relaxed (12 lines changed), Iron (35 lines changed; this includes some code cleanup).