diff options
| author | Cyril Cohen | 2020-11-20 02:31:40 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-20 20:50:44 +0100 |
| commit | c55acd1fefa970cc4ed3a8a53b05fd77008a7cdf (patch) | |
| tree | 864b98bd44a865c6155e96746a4c837061a51888 /CHANGELOG_UNRELEASED.md | |
| parent | fd0d84084738decce3fb6557cf82dc10d030daa8 (diff) | |
Tuning simplifications using Arguments simpl nomatch
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f2ba40b..4de594e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -294,6 +294,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, added `size_merge_sort_push`, which documents an invariant of `merge_sort_push`. +- in `seq.v ` added lemma `mask0s`. + ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 @@ -374,6 +376,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `order.v`, generalized `sort_le_id` for any `porderType`. +- the following constants have been tuned to only reduce when they do + not expose a match: `subn_rec`, `decode_rec`, `nth` (thus avoiding a + notorious problem of ``p`_0`` expanding too eagerly), `set_nth`, + `take`, `drop`, `eqseq`, `incr_nth`, `elogn2`, `binomial_rec`, + `sumpT`. + +- in `seq.v`, `mask` will only expand if both arguments are + constructors, the case `mask [::] s` can be dealt with using + `mask0s` or explicit conversion. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) |