Skip to content

Commit

Permalink
Merge branch 'master' of github.com:PrincetonUniversity/VST
Browse files Browse the repository at this point in the history
  • Loading branch information
andrew-appel committed Mar 14, 2024
2 parents b95bddc + cc77d15 commit 3fd74e2
Showing 1 changed file with 13 additions and 0 deletions.
13 changes: 13 additions & 0 deletions CHANGES
Original file line number Diff line number Diff line change
@@ -1,3 +1,16 @@
CHANGES SINCE LAST RELEASE (udpated March 2024)

- repr_inj handles int64 compares better
- Added nonempty_writable_glb lemma for user convenience (#734)
- Remove unnecessary premise in field_at_app lemma (#743)
- Improve error message in forward_if (#744)
- Fix slow unification in load/store forward tactics (#748)
- Generalize permission share in data_at_in_or_ptr_int lemma (etc.) (#749)
- Improve error messages from deadvars tactic (#751)
- Fix issue #745 (minor bug in entailer tactic)
- Localize/unlocalize more robust regarding unification vars (#756)
- Ensure veric.version is present in opam distributions

CHANGES IN RELEASE 2.13 (October 2023)

- Improved error diagnostics when compspecs mismatch
Expand Down

0 comments on commit 3fd74e2

Please sign in to comment.