Skip to content
Snippets Groups Projects
Commit c9154d43 authored by Ralf Jung's avatar Ralf Jung
Browse files

add more credit in changelog

parent 036358a3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
CHANGELOG.md
+ 2
− 0
View file @ c9154d43
...@@ -42,6 +42,7 @@ Coq 8.11 is no longer supported in this version of Iris. ...@@ -42,6 +42,7 @@ Coq 8.11 is no longer supported in this version of Iris.
view and per-element points-to facts written `k ↪[γ] w`. view and per-element points-to facts written `k ↪[γ] w`.
* Generalize the soundness lemma of the base logic `step_fupdN_soundness`. * Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
It applies even if invariants stay open accross an arbitrary number of laters. It applies even if invariants stay open accross an arbitrary number of laters.
(by Jacques-Henri Jourdan)
**Changes in `program_logic`:** **Changes in `program_logic`:**
...@@ -58,6 +59,7 @@ Coq 8.11 is no longer supported in this version of Iris. ...@@ -58,6 +59,7 @@ Coq 8.11 is no longer supported in this version of Iris.
- Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`. - Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
- Some proofs using lifting lemmas and adequacy theorems need to be adapted - Some proofs using lifting lemmas and adequacy theorems need to be adapted
to ignore the new step counter. to ignore the new step counter.
(by Jacques-Henri Jourdan)
* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement. * Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement.
**Changes in `heap_lang`:** **Changes in `heap_lang`:**
......
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