diff options
| author | Théo Zimmermann | 2020-05-12 10:08:29 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-12 10:08:29 +0200 |
| commit | 007ed9e21f69a157ffff3fa5f990f62ab2756416 (patch) | |
| tree | 2cdeda8cae496fc731ab202c61e50014b4b4218e | |
| parent | 00328b2165b68c81eef0a6bf1c5483f8e906a31d (diff) | |
| parent | 9f5a604dacd0fd335559b573f93b04bf6033d1cd (diff) | |
Merge PR #12303: [changelog] Fuse changelogs for #11249 and #12237
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst | 7 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/12237-list-more-filter-incl.rst | 4 |
2 files changed, 4 insertions, 7 deletions
diff --git a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst index be15fbf8f5..be54e45808 100644 --- a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst +++ b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst @@ -7,11 +7,12 @@ - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt`` - properties of ``concat``: ``in_concat``, ``remove_concat`` - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map`` - - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl`` + - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff`` + - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl`` - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall`` - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat`` - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt`` - - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``NoDup_rev``, ``nodup_incl``, ``cons_seq``, ``seq_S`` + - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S`` - (`#11249 <https://github.com/coq/coq/pull/11249>`_, + (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_, by Olivier Laurent). 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 deleted file mode 100644 index 37aaf697b5..0000000000 --- a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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). |