Commit c3aae082 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix changelog order

parent dce194f3
......@@ -25,6 +25,12 @@ lemma.
* Demote the Camera structure on `list` to `iris_staging` since its composition
is not very well-behaved.
**Changes in `proof_mode`:**
* Add support for pure names `%H` in intro patterns. This is now natively
supported whereas the previous experimental support required installing
https://gitlab.mpi-sws.org/iris/string-ident.
**Changes in `base_logic`:**
* Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
......@@ -52,12 +58,6 @@ lemma.
* Rename `Build_loc` constructor for `loc` type to `Loc`.
**Changes in `proof_mode`:**
* Add support for pure names `%H` in intro patterns. This is now natively
supported whereas the previous experimental support required installing
https://gitlab.mpi-sws.org/iris/string-ident.
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment