Coq 8.10.1

Announcements
1

The 8.10.1 release of Coq 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.

Feedback and bug reports are extremely welcome.

2 Likes