Commit c8a79f5a authored by Robbert Krebbers's avatar Robbert Krebbers

Add changelog entry.

parent c7cd43a3
......@@ -164,6 +164,8 @@ Changes in Coq:
* Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
`Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
`cmra_morphism_core`.
* Rename lemmas `fupd_big_sep{L,M,S,MS}` into `big_sep{L,M,S,MS}_fupd` to be
consistent with other such big op lemmas. Also add such lemmas for `bupd`.
* Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
`-d>`. The renaming can be automatically done using the following script (on
......
Markdown is supported
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