Instances for empty type.

[arthuraa]

Motivation for this change

Several users have expressed their wish for an empty type in mathcomp (e.g. #225). This PR adds a void notation for the Empty_set type of the standard library, along with instances of basic classes.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

The documentation already existed in eqtype. I have added a note in fintype, but left choice alone since the instance list there was not exhaustive.

The notation is defined in ssrfun. Since most of this file lives in the Coq source now, I did not add a corresponding entry there. Would it make sense to do so?

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[CohenCyril]

LGTM

[amahboubi]

Hi @arthuraa, thanks for your contribution! Regarding your question:

The notation is defined in ssrfun. Since most of this file lives in the Coq source now, I did not add a corresponding entry there. Would it make sense to do so?

I think you should add a header to mathcomp's ssrfun, since you introduced the notation here. This is what happens, e.g., in file ssreflect.v. I will merge as soon as you add this documentation.

[arthuraa]

@amahboubi Sounds good! How does this look?

[amahboubi]

It looks great.

[CohenCyril]

Oh, but if you add something to the local ssrfun you should also add it to Coq's... did you? If not, could you do it?

[arthuraa]

@CohenCyril Just did: coq/coq#10932.

[amahboubi]

@CohenCyril, the PR has been merged in Coq. Anything else you would like @arthuraa to do before we merge?

[CohenCyril]

@amahboubi nothing more, LGTM, we can merge