From 1b3e86bb788848e4484be832d28c8e3e965453d7 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 18 Mar 2023 10:20:27 +0100 Subject: [PATCH] Remove redundant space. --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 185bb7e89..43ed2e393 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -36,7 +36,7 @@ Coq 8.13 is no longer supported. * Use `binder` in notations for big ops. This means one can write things such 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). + 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 `◇`. -- GitLab