From 6dd07f2af08414fff016da7dddc8381fcccec3eb Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 28 Aug 2023 19:32:25 +0200 Subject: [PATCH] changelog --- CHANGELOG.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index dd1cf310a..2482b3d14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -152,7 +152,7 @@ Coq 8.13 is no longer supported. `iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre) * Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See - [iris/proofmode/base.v](proofmode/base.v) for documentation on how + [proofmode/base.v](iris/proofmode/base.v) for documentation on how to use these tactics to convert your own fixed arity tactics to an n-ary variant. @@ -181,6 +181,10 @@ Coq 8.13 is no longer supported. * Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`. * Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim) +* Make the generic `lock` specification a typeclass. Code that is generic about + lock implementations, or that instantiates that specification, needs + adjustment. See [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for + documentation on how to work with this specification. **LaTeX changes:** -- GitLab