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

CHANGELOG.

parent 83448f76
No related branches found
No related tags found
1 merge request!293Make `done` work on `is_Some`.
Pipeline #50419 passed
......@@ -108,6 +108,7 @@ API-breaking change is listed.
- Rename `insert_delete``insert_delete_insert`; add new `insert_delete` that
is consistent with `delete_insert`.
- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
- Make `done` work on goals of the form `is_Some`.
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