Avoid relying on `Export` bugs

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.

closed

Subsumed by c579b46c

Thanks for the MR.

It's really weird that it picked the version in Morphisms, it should always pick the std++ one if anything from std++ is imported. So, I would say that Coq's "new" behavior is good.

I see, thanks for the improved version of the patch!