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.
---
 plugins/decl_mode/decl_mode_plugin.mlpack | 5 -----
 1 file changed, 5 deletions(-)
 delete mode 100644 plugins/decl_mode/decl_mode_plugin.mlpack

(limited to 'plugins/decl_mode/decl_mode_plugin.mlpack')

diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
deleted file mode 100644
index 1b84a0790f..0000000000
--- a/plugins/decl_mode/decl_mode_plugin.mlpack
+++ /dev/null
@@ -1,5 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode
-- 
cgit v1.2.3