From 74eb80a663cb1e45147a67dfa8c190547ee850e2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 8 Nov 2020 00:25:59 +0100 Subject: Shorter proofs and suggestions by Kazuhiko Co-authored-by: Kazuhiko Sakaguchi --- CHANGELOG_UNRELEASED.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'CHANGELOG_UNRELEASED.md') diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 073464c..c4abdf3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,8 +228,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `commCmx`. The common arguments of these lemmas `R` and `n` are maximal implicits. - - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, - `subset_maskP`, `subset_subseqP`, `count_rem`, `count_mem_rem`, + - in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, `undup_subseq`, + `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, `rem_cons`, `remE`, `subseq_rem` and `leq_count_uniq`. - in `fintype.v`, added `mask_enum_ord`. - in `bigop.v`, added `big_mask_tuple` and `big_mask`. -- cgit v1.2.3