Skip to content
Snippets Groups Projects
Commit 74ed6cfa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent e400a5b1
No related branches found
No related tags found
1 merge request!594split up list.v into smaller files
Pipeline #119736 passed
......@@ -23,6 +23,9 @@ API-breaking change is listed.
implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
and also considered part of the list module, so existing imports should be
updated.
- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
functions; they existed solely to facilitate the proofs of decidability of
`submseteq` and `≡ₚ`, which have been refactored.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment