From e703b4c94bc283da3b418ead818288b1bd1a5b20 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 4 May 2021 10:05:17 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5556ab79..cae81682 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,7 @@ API-breaking change is listed.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
 - Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
+- Add `option_guard_True_pi`.
 
 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