1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 7956db6f5..c25649823 100644
--- a/CHANGES
+++ b/CHANGES
@@ -105,6 +105,7 @@ Other bugfixes
 - #4882: anomaly with Declare Implicit Tactic on hole of type with evars
 - Fix use of "Declare Implicit Tactic" in refine.
   triggered by CoqIDE
+- #4069, #4718: congruence fails when universes are involved.
 
 Universes
 - Disallow silently dropping universe instances applied to variables