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.
---
 test-suite/bugs/closed/2640.v | 17 -----------------
 1 file changed, 17 deletions(-)
 delete mode 100644 test-suite/bugs/closed/2640.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v
deleted file mode 100644
index da0cc68a4e..0000000000
--- a/test-suite/bugs/closed/2640.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Testing consistency of globalization and interpretation in some
-   extreme cases *)
-
-Section sect.
-
-  (* Simplification of the initial example *)
-  Hypothesis Other: True.
-
-  Lemma C2 : True.
-  proof.
-  Fail have True using Other.
-  Abort.
-
-  (* Variant of the same problem *)
-  Lemma C2 : True.
-  Fail clear; Other.
-  Abort.
-- 
cgit v1.2.3