From 8b71b075c0e1b34ef40ab865f28a89c7d4d16b6c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sun, 5 Mar 2023 10:31:06 +0100 Subject: [PATCH] CHANGELOG entry. --- CHANGELOG.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3330e7f25..a25e051f7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,12 @@ Coq 8.13 is no longer supported. as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y âŒ`. * Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step closure of a PROP-level binary relation. (by Simcha van Collem). +* Make the `unseal` tactic of `monPred` more consistent with `uPred`: + + Rename `MonPred.unseal` → `monPred.unseal` + + No longer unfold derived BI connectives `<affine>`, `<absorb>` and `â—‡`. + * Make `monPred.unseal` tactic more robust by using types to unfold the right + BI projections. +* Add `unseal` tactic for `siProp`. **Changes in `proofmode`:** @@ -62,6 +68,8 @@ Coq 8.13 is no longer supported. * Add `IsExcept0` instance for invariants, allowing you to remove laters of timeless hypotheses when proving an invariant (without an update). +* Make `uPred.unseal` tactic more robust by using types to unfold the right + BI projections. **Changes in `heap_lang`:** @@ -85,6 +93,8 @@ s/\bsig_dist_alt\b/sig_dist_def/g # Loc s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g +# unseal +s/\bMonPred\.unseal\b/monPred\.unseal/g EOF ``` -- GitLab