Farewell decl_mode

This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.

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
 ==============================