Adapt to rocq#21180

[Tragicus]

In one of the tests, rocq-prover/rocq#21180 encounters a non-pattern fragment unification problem and produces an eta-expansion that breaks Rocq-Elpi's unifier.

[Tragicus]

This is a bit weird because the point of the eta-expansion is to make an evar instantiation succeed by making another evar forget one of its arguments. Yet, once the arguments make it into the second evar's context, the algorithm stops complaining about them and leaves them be. It would be best to detect this and make the instantiation work without absorbing the arguments, but I am not sure if there is a way to do this.

[gares]

I had the impression Rocq's evars had a filter on the context to implement pruning without having to assign them (to a lambda ignoring the argument).

[Tragicus]

If I understand correctly, that is for the arguments that are already in the context of the evar, not those that the evar is applied to.

[gares]

Yes. Oh, I think I misread the test. I think it should be lp:(K u) and not (lp:K u), as you changed it.
But once you do that, I don't see why the evar would not have u in its scope.

IMO the old test had a mistake. Fixing that still requires the call to unify-eq?

[Tragicus]

You need K : term for K = global GR to typecheck.

[gares]

I think I see now what you are doing. Maybe

(pi u\ X u = app[global GR,u]) % Rocq <= 9.1
;
(pi u\ X u = app[(fun _ _ _\ app[global GR,u]),_]) % Rocq > 9.1

[gares]

Anyway, the test checks that the "magic record constructor" of mathcomp infers Ord. If now it infers something different, it may have consequences in MC as well.

[Tragicus]

That also works.