-
Ana de Almeida Borges authored
Also works with MathComp 1.15 and 1.17 No longer works with Coq 8.13 and below, since the export attribute didn't exist back then. This requires MathComp at least 1.13, since 1.12 is not compatible with Coq 8.14.
Also works with MathComp 1.15 and 1.17 No longer works with Coq 8.13 and below, since the export attribute didn't exist back then. This requires MathComp at least 1.13, since 1.12 is not compatible with Coq 8.14.