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.