1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 4a7cb8c45e..ba4ac74a5b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ Tactics
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
 
+Code removed
+
+- The mathematical proof language (also known as declarative mode)
+
 Changes from V8.6beta1 to V8.6
 ==============================