Validate
The validate make target outputs as axioms things from Mathcomp that are in fact proved but enclosed in opaque modules.
This is a known bug in coqchk : https://github.com/coq/coq/issues/5030 unfortunately not trivial to fix. I'll try to have a look at some point. Just putting this here so that I don't forget.