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

Add CHANGELOG.

parent 71dd79c3
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 @ 3466b794
...@@ -70,6 +70,8 @@ Coq 8.13 is no longer supported. ...@@ -70,6 +70,8 @@ Coq 8.13 is no longer supported.
timeless hypotheses when proving an invariant (without an update). timeless hypotheses when proving an invariant (without an update).
* Make `uPred.unseal` tactic more robust by using types to unfold the right * Make `uPred.unseal` tactic more robust by using types to unfold the right
BI projections. BI projections.
* Turn `internal_eq_entails` into a bi-implication.
* Add lemmas to relate internal/external non-expansiveness and contractiveness.
**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