Skip to content

Make trivial instances explicit

Maxime Dénès requested to merge maximedenes/iris-coq:instance-nobody-open-proof into master

This is in preparation for coq/coq#9274.

Like the one on stdpp, this patch should be backward compatible, but that should be tested.

Merge request reports