Coq 8.8.0 is out

The final release of Coq 8.8.0 is available. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.