Make trivial instances explicit

This is in preparation for coq/coq#9274.

Should be backward compatible but that remains to be tested.

Thanks for the MR.

@jung To test for backwards compatibility, what's the easiest way to run this on all versions tested by our CI?

Uh. One of us pushing it to a ci/ branch, I guess.

FYI, I'm preparing a similar patch against Iris.

Uh. One of us pushing it to a ci/ branch, I guess.

Done that, the CI is running now.

The CI passed, merging!

mentioned in commit 17241997

merged

mentioned in merge request iris!1035 (merged)