Coq 8.10.0 contains:
- some quality-of-life bug fixes;
- a critical bug fix related to template polymorphism;
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositions: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
All details can be found in the user manual.