Skip to content

Make trivial instances explicit

This is in preparation for coq/coq#9274.

Again, should be backward compatible but I haven't tested.

Merge request reports