Coq 8.10+beta3 is out
The third beta release of Coq 8.10 is available for testing.
This third β version includes various bug fixes and improvements, including:
- improved warning on coercion path ambiguity;
- support for OCaml extraction of primitive machine integers;
- fix for the soundness issue with template polymorphism;
- fix extraction of dependent record projections to OCaml.
More details are given in the user manual.
Feedback and bug reports are extremely welcome.