From ab2ec90b51c764f09b13ff2e890329814f2b7281 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 16 Feb 2023 12:14:00 +0100 Subject: [PATCH] Tweak CHANGELOG, give credit to @svancollem. --- CHANGELOG.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5eb8ef8e3..5be61aab7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,12 +18,10 @@ Coq 8.13 is no longer supported. **Changes in `bi`:** -* Add a construction `bi_tc` to create transitive closures of - PROP-level binary relations. * Use `binder` in notations for big ops. This means one can write things such as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y âŒ`. -* Add a construction `bi_nsteps` to create an `n`-step closure of a - PROP-level binary relation. +* Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step + closure of a PROP-level binary relation. (by Simcha van Collem). **Changes in `proofmode`:** -- GitLab