diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
| commit | 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 (patch) | |
| tree | 1009560f396c397caa537471fc922aa0fb2af0bf /test-suite/complexity | |
| parent | e3567014035a55cfde44099ce59d142d084faac5 (diff) | |
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
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/autodecomp.v | 11 |
1 files changed, 0 insertions, 11 deletions
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. |