# Coq 8.10.2

**URL:** <https://discourse.rocq-prover.org/t/coq-8-10-2/511>\
**Category:** Announcements\
**Created:** [November 29, 2019, 10:58am UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511 "2019-11-29T10:58:07Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Vincent](https://avatars.discourse-cdn.com/v4/letter/v/e9bcb4/32.png) [@Vincent](https://discourse.rocq-prover.org/u/Vincent)\
**Post date:** [November 29, 2019, 10:58am UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511/1 "2019-11-29T10:58:07Z")

</div>

The [8.10.2 release of Coq](https://github.com/coq/coq/releases/tag/V8.10.2) is available.

Main changes:

- Fixed a critical bug of template polymorphism and nonlinear universes
- Fixed a few anomalies
- Fixed an 8.10 regression related to the printing of coercions associated to notations
- Fixed uneven dimensions of CoqIDE panels when window has been resized
- Fixed queries in CoqIDE

All details can be found in the [user manual](https://coq.github.io/doc/V8.10.2/refman/changes.html#changes-in-8-10-2).

Feedback and [bug reports](https://github.com/coq/coq/issues) are extremely welcome.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [November 29, 2019, 2:56pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511/2 "2019-11-29T14:56:00Z")

</div>

FWIW, it’s also coming on opam: [https://github.com/ocaml/opam-repository/pull/15416](https://github.com/ocaml/opam-repository/pull/15416), [https://github.com/ocaml/opam-repository/pull/15417](https://github.com/ocaml/opam-repository/pull/15417).

---

<div class="post-metadata">

**Author:** ![Alice](https://avatars.discourse-cdn.com/v4/letter/a/779978/32.png) [@Alice](https://discourse.rocq-prover.org/u/Alice)\
**Post date:** [December 5, 2019, 4:12pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511/3 "2019-12-05T16:12:29Z")

</div>

Excuse me, I’m learning to use coq recently. I have a project based on 8.4, but now I want to port to 8.10.2. I know that the changes between these two versions are large, but can you give me some suggestions about Migration issue? thank you very much!

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [December 5, 2019, 4:14pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511/4 "2019-12-05T16:14:47Z")

</div>

Your best bet is doing the migration one-version-at-a-time; depending on the ltac hackery you are using it should be easy or pretty hard; expect the most trouble in the jump from 8.4 to 8.5 tho, the rest should be doable as long as you read the `Changelog`; if you find some problem you don’t understand you can ask the devs here or in Gitter.

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [December 6, 2019, 2:03pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-2/511/5 "2019-12-06T14:03:35Z")

</div>

Complete changelog, from 8.4 to 8.10 can be found here: [https://coq.inria.fr/refman/changes.html](https://coq.inria.fr/refman/changes.html)