diff --git a/CHANGELOG.md b/CHANGELOG.md index 6079cf56fa649bafcc6c0b8385b094c39f4a9e67..5f21ae986b558e881fe73f42db558d3f475bf8ee 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,19 @@ This file lists "large-ish" changes to the std++ Coq library, but not every API-breaking change is listed. +## std++ 1.2.1 (unreleased) + +This release of std++ received contributions by Michael Sammler, Paolo +G. Giarrusso, Ralf Jung, Robbert Krebbers, and Simon Spies. + +Noteworthy additions and changes: + +- `max` and `min` infix notations for `N` and `Z` like we have for `nat`. +- Make `solve_ndisj` tactic more powerful. +- Add typeclass `Involutive`. +- Improved `naive_solver` performance in case the goal is trivially solvable. +- A bunch of new lemmas for list operations. + ## std++ 1.2.0 (released 2019-04-26) Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use