# Coq 8.10.1

**URL:** <https://discourse.rocq-prover.org/t/coq-8-10-1/488>\
**Category:** Announcements\
**Created:** [October 25, 2019, 8:57pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-1/488 "2019-10-25T20:57:21Z")\
**Posts on this page:** 1\
**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:** [October 25, 2019, 8:57pm UTC](https://discourse.rocq-prover.org/t/coq-8-10-1/488/1 "2019-10-25T20:57:21Z")

</div>

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

Main changes:

- fix proof of False when using SProp;
- fix an anomaly when unsolved evar in Add Ring;
- fix Ltac regression in binding free names in uconstr;
- fix handling of unicode input before space;
- fix custom extraction of inductives to JSON.

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

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