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

CHANGELOG.

parent eeae7519
No related tags found
No related merge requests found
...@@ -23,6 +23,7 @@ API-breaking change is listed. ...@@ -23,6 +23,7 @@ API-breaking change is listed.
- Add `inv` tactic as a more well-behaved alternative to `inversion_clear` - Add `inv` tactic as a more well-behaved alternative to `inversion_clear`
(inspired by CompCert), and `oinv` as its version on open terms. (inspired by CompCert), and `oinv` as its version on open terms.
- Add `prod_swap : A * B → B * A` and some basic theory about it. - Add `prod_swap : A * B → B * A` and some basic theory about it.
- Add lemma `lookup_total_fmap`.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (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