From 8b8653b82def87861566fe44ad88439ab14aec75 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 14 Jul 2020 11:11:25 +0200
Subject: [PATCH] edit and fix changelog
---
CHANGELOG.md | 29 ++++++++++++++++-------------
1 file changed, 16 insertions(+), 13 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4ecf138e..7bf98fad 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,26 +3,34 @@ API-breaking change is listed.
## std++ master
-Coq 8.7 is no longer supported by this release.
+Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
- Rename `Z2Nat_inj_div` and `Z2Nat_inj_mod` to `Nat2Z_inj_div` and
`Nat2Z_inj_mod` to follow the naming convention of `Nat2Z` and
- `Z2Nat`. The names `Z2Nat_inj_div` and `Z2Nat_inj_mod` have been
- repurposed for be the lemmas they should actually be.
-- Added `rotate` and `rotate_take` functions for accessing a list with
- wrap-around. Also added `rotate_nat_add` and `rotate_nat_sub` for
+ `Z2Nat`. Re-purpose the names `Z2Nat_inj_div` and `Z2Nat_inj_mod` for be the
+ lemmas they should actually be.
+- Add `rotate` and `rotate_take` functions for accessing a list with
+ wrap-around. Also add `rotate_nat_add` and `rotate_nat_sub` for
computing indicies into a rotated list.
-- Added the `select` and `revert select` tactics for selecting and
+- Add the `select` and `revert select` tactics for selecting and
reverting a hypothesis based on a pattern.
-- Extracted `list_numbers.v` from `list.v` and `numbers.v` for
+- Extract `list_numbers.v` from `list.v` and `numbers.v` for
functions, which operate on lists of numbers (`seq`, `seqZ`,
`sum_list(_with)` and `max_list(_with)`). `list_numbers.v` is
exported by the prelude. This is a breaking change if one only
imports `list.v`, but not the prelude.
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
-- Added `Countable` instance for `Ascii.ascii`.
+- Add `Countable` instance for `Ascii.ascii`.
- Make lemma `list_find_Some` more apply friendly.
+- Add `filter_app` lemma.
- Add tactic `multiset_solver` for solving goals involving multisets.
+- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
+ `singletonM` and to avoid overlap with `sets.singleton_proper`.
+- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
+- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
+ as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
+- Fix list `Datatypes.length` and string `strings.length` shadowing (`length`
+ should now always be `Datatypes.length`).
## std++ 1.3 (released 2020-03-18)
@@ -76,11 +84,6 @@ Noteworthy additions and changes:
`seqZ_lookup_ge` → `lookup_seqZ_ge`, and `seqZ_lookup` → `lookup_seqZ`
+ Rename `lookup_seq_inv` → `lookup_seq` and generalize it to a bi-implication
+ Add `NoDup_seqZ` and `Forall_seqZ`
-- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
- `singletonM` and to avoid overlap with `sets.singleton_proper`.
-- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
-- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
- as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
--
GitLab