Fix priority of `Permutation_app'`.

This is a workaround for https://github.com/coq/coq/issues/14571

This fixes #114 (closed).

This fixes a regression caused by !270 (merged).

LGTM.

There's no way we can test for this, is there? Like, do eauto with the typeclasses DB with a small amount of fuel that would not suffice for the 85k trace that arises in #114 (closed)?

No idea, but if it's possible, such tests also seem very fragile.

@jung Do you still want a CHANGELOG entry? Note that the bug did not exist in the latest released std++ (which did not contain !270 (merged)), so the CHANGELOG entry will be rather weird :).

It turns out a bunch of other Proper instances for Permutation also have priority 10 (which means they are used after proper_relation). Maybe we should fix those too in std++? For example: NoDup and cons.

See https://github.com/coq/coq/issues/14571#issuecomment-870463360

added 1 commit

• cb429ab7 - Also fix `Permutation_cons`.

Compare with previous version

I also fixed cons since we also replaced std++'s custom instance with the stdlib instance in !270 (merged).

We have our own NoDup, so the priority of Coq stdlib's NoDup is irrelevant.

Just please make sure to properly add comments explaining all this. :)

LGTM.

In regards to testing I only think keeping track of the compile time of larger developments (like Iris) makes sense.

And instruct people to look for and report these kind of things in their own developments.

Let's wait with merging to see if the Coq bench https://github.com/coq/coq/pull/14574 gives any regressions.

resolved all threads

resolved all threads

Going to merge.

merged

mentioned in commit 40a943ea