Merge in mathcomp proper

arthuraa / coq-void

Mathcomp instances for the empty type

MIT License

0 stars 0 forks source link

Merge in mathcomp proper #1

Open gares opened 4 years ago

gares commented 4 years ago

At the last math comp meeting we discussed about this code, and we believe it makes sense to merge it in mathcomp. Would you agree?

arthuraa commented 4 years ago

Yes, I think it would be great. Do you mean adding the instances at the corresponding files in ssreflect, or as a separate project under the mathcomp page?

gares commented 4 years ago

I'm talking about a pull request github.com/math-comp/math-comp

arthuraa commented 4 years ago

That sounds good. I'll put something up.

anton-trunov commented 4 years ago

This is done in https://github.com/math-comp/math-comp/pull/393