From dcbd66a5f04b7afabb073c32a505ad1d61bd1416 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 29 Feb 2024 17:48:41 +0100 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index d5e6f775..a604255c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,6 +27,7 @@ Coq 8.19 is newly supported by this version of std++. These tactics support both named hypotheses (`inv H`) and using a number to refer to a hypothesis on the goal (`inv 1`). - Add `prod_swap : A * B → B * A` and some basic theory about it. +- Add lemma `join_app`. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). -- GitLab