diff options
| author | Hugo Herbelin | 2020-05-09 15:07:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-09 15:07:31 +0200 |
| commit | 86afb971718d856007f503c9f059532ccbd3f5a5 (patch) | |
| tree | 78540c62cfb57f64c897fb905a75b779178cda12 /doc | |
| parent | 56e2d2fe23bfe69f7c181e3786e8e95f1ee6151b (diff) | |
| parent | 1a11eaddca057bea4e1ea0b3c276fc5228e5b4b2 (diff) | |
Merge PR #12237: [stdlib] [List] add results around incl, filter and nth
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12237-list-more-filter-incl.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst new file mode 100644 index 0000000000..37aaf697b5 --- /dev/null +++ b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst @@ -0,0 +1,4 @@ +- **Added:** + new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff`` + (`#12237 <https://github.com/coq/coq/pull/12237>`_, + by Olivier Laurent). |