Skip to content

@vbgl vbgl released this Sep 16, 2019 · 22 commits to v8.10 since this release

This is the third β version of Coq 8.10.

Compared to the previous one, it includes various bug fixes, 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.

Assets 6
You can’t perform that action at this time.