From 03b631ea3eeeaab9054c34d9121c0a75fabea72c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Oct 2014 18:02:10 +0200
Subject: Removing test for bug #2080.

Naming a Ltac definition like a built-in tactic used to fail, but now only
spits out a warning. This is too complicated to test...
---
 test-suite/bugs/closed/2080.v | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 test-suite/bugs/closed/2080.v

diff --git a/test-suite/bugs/closed/2080.v b/test-suite/bugs/closed/2080.v
deleted file mode 100644
index 62c42c8c31..0000000000
--- a/test-suite/bugs/closed/2080.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail Ltac clear h := inversion h; clear h.
-- 
cgit v1.2.3