1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 540b3fe30d..d0931f897f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -44,6 +44,8 @@ Tactics
 - Tactic autorewrite does no longer instantiate pre-existing
   existential variables (theoretical source of possible incompatibility).
 - Tactic "dependent rewrite" now supports equality in "sig".
+- Tactic omega now understands Zpred (wish #1912) and can prove any goal
+  from a context containing an arithmetical contradiction (wish #2236).
 
 Vernacular commands