From 716397754c44432530195b92cbde6ba83c16045e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 9 Aug 2024 23:31:24 +0900
Subject: [PATCH] fix

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bb7e2df67..77e7ac33c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,12 @@ Latest releases: [[1.3.1] - 2024-08-09](#131---2024-08-09) and [[1.3.0] - 2024-0
 
 ## [1.3.1] - 2024-08-09
 
+### Changed
+
+- in `wochoice.v`:
+  + two applications of the lemma `in3W` have been removed because they seem to cause
+    a universe inconsistency when one loads the `ring` module of `algebra-tactics`
+
 ### Generalized
 
 - in `reals.v`: