From ca82e1ff51108a3dac37f52a96f3af4b4e8d1a18 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Mar 2017 11:18:29 +0100
Subject: Farewell decl_mode

This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

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
 ==============================
 
-- 
cgit v1.2.3