From 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 23 Apr 2012 18:51:11 +0000
Subject: remove undocumented and scarcely-used tactic auto decomp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/complexity/autodecomp.v | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 test-suite/complexity/autodecomp.v

(limited to 'test-suite/complexity')

diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
deleted file mode 100644
index 85589ff79..000000000
--- a/test-suite/complexity/autodecomp.v
+++ /dev/null
@@ -1,11 +0,0 @@
-(* This example used to be in (at least) exponential time in the number of
-   conjunctive types in the hypotheses before revision 11713 *)
-(* Expected time < 1.50s *)
-
-Goal
-True/\True->
-True/\True->
-True/\True->
-False/\False.
-
-Timeout 5 Time auto decomp.
-- 
cgit v1.2.3