diff options
| author | Cyril Cohen | 2020-11-18 11:34:48 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-18 11:34:48 +0100 |
| commit | 0606b6bf22e258dc3b7cf440f10c108f785904b5 (patch) | |
| tree | 615dbcedea36f9179eceb4f8ef9aa3e4a996c402 /CHANGELOG_UNRELEASED.md | |
| parent | 831e7a2d2d7c5385751946582ede7f766accca58 (diff) | |
| parent | 8eb486ad82accfb1417be11ecc2889aa09c22081 (diff) | |
Merge pull request #651 from CohenCyril/merge_sort_push_invariant
Adding size_merge_sort_push
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8cb8d9c..ac8ce25 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -289,6 +289,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `fullrowsub_free`, `mxrank_fullrowsub`, `eq_fullrowsub`, and `fullrankfun_inj`. +- in `path.v`, added `size_merge_sort_push`, which documents an + invariant of `merge_sort_push`. + ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 |