Skip to content

Avoid relying on `Export` bugs

Maxime Dénès requested to merge maximedenes/stdpp:fix-export into master

See https://github.com/coq/coq/issues/10480 and https://github.com/coq/coq/issues/10474.

This should be compatible with Coq's master, but I haven't tested.

Merge request reports