Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7

147 files changed, 0 insertions, 14 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1041.v b/test-suite/bugs/closed/1041.v
index a5de82e0d..a5de82e0d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1041.v
+++ b/test-suite/bugs/closed/1041.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/1100.v
index 32c78b4b9..32c78b4b9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1100.v
+++ b/test-suite/bugs/closed/1100.v
diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/121.v
index 8c5a38859..8c5a38859 100644
--- a/test-suite/bugs/closed/shouldsucceed/121.v
+++ b/test-suite/bugs/closed/121.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1243.v b/test-suite/bugs/closed/1243.v
index 7d6781db2..7d6781db2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1243.v
+++ b/test-suite/bugs/closed/1243.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/1302.v
index e94dfcfb0..e94dfcfb0 100644
--- a/test-suite/bugs/closed/shouldsucceed/1302.v
+++ b/test-suite/bugs/closed/1302.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/1322.v
index 1ec7d452a..1ec7d452a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1322.v
+++ b/test-suite/bugs/closed/1322.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/1411.v
index a1a7b288a..a1a7b288a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/1411.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/1414.v
index ee9e2504a..ee9e2504a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/1414.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/1416.v
index ee0920057..ee0920057 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/1416.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/1419.v
index d021107d1..d021107d1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1419.v
+++ b/test-suite/bugs/closed/1419.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/1425.v
index 6be30174a..6be30174a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1425.v
+++ b/test-suite/bugs/closed/1425.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/1446.v
index 8cb2d653b..8cb2d653b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1446.v
+++ b/test-suite/bugs/closed/1446.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/1448.v
index fe3b4c8b4..fe3b4c8b4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1448.v
+++ b/test-suite/bugs/closed/1448.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/1477.v
index dfc8c3280..dfc8c3280 100644
--- a/test-suite/bugs/closed/shouldsucceed/1477.v
+++ b/test-suite/bugs/closed/1477.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1483.v b/test-suite/bugs/closed/1483.v
index a3d7f1683..a3d7f1683 100644
--- a/test-suite/bugs/closed/shouldsucceed/1483.v
+++ b/test-suite/bugs/closed/1483.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/1507.v
index f2ab91003..f2ab91003 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/1507.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/1568.v
index 3609e9c83..3609e9c83 100644
--- a/test-suite/bugs/closed/shouldsucceed/1568.v
+++ b/test-suite/bugs/closed/1568.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/1576.v
index 3621f7a1f..3621f7a1f 100644
--- a/test-suite/bugs/closed/shouldsucceed/1576.v
+++ b/test-suite/bugs/closed/1576.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/1582.v
index be5d3dd21..be5d3dd21 100644
--- a/test-suite/bugs/closed/shouldsucceed/1582.v
+++ b/test-suite/bugs/closed/1582.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/1604.v
index 22c3df824..22c3df824 100644
--- a/test-suite/bugs/closed/shouldsucceed/1604.v
+++ b/test-suite/bugs/closed/1604.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1614.v b/test-suite/bugs/closed/1614.v
index 6bc165d40..6bc165d40 100644
--- a/test-suite/bugs/closed/shouldsucceed/1614.v
+++ b/test-suite/bugs/closed/1614.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/1618.v
index a9b067ceb..a9b067ceb 100644
--- a/test-suite/bugs/closed/shouldsucceed/1618.v
+++ b/test-suite/bugs/closed/1618.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/1634.v
index 0150c2503..0150c2503 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/1634.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/1643.v
index 879a65b18..879a65b18 100644
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ b/test-suite/bugs/closed/1643.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1680.v b/test-suite/bugs/closed/1680.v
index 524c7bab4..524c7bab4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1680.v
+++ b/test-suite/bugs/closed/1680.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/1683.v
index 3e99694b3..3e99694b3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1683.v
+++ b/test-suite/bugs/closed/1683.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/1696.v
index 0826428a3..0826428a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1696.v
+++ b/test-suite/bugs/closed/1696.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/1704.v
index 4b02d5f93..4b02d5f93 100644
--- a/test-suite/bugs/closed/shouldsucceed/1704.v
+++ b/test-suite/bugs/closed/1704.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1711.v b/test-suite/bugs/closed/1711.v
index e16612e38..e16612e38 100644
--- a/test-suite/bugs/closed/shouldsucceed/1711.v
+++ b/test-suite/bugs/closed/1711.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1718.v b/test-suite/bugs/closed/1718.v
index 715fa9419..715fa9419 100644
--- a/test-suite/bugs/closed/shouldsucceed/1718.v
+++ b/test-suite/bugs/closed/1718.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/1738.v
index c2926a2b2..c2926a2b2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1738.v
+++ b/test-suite/bugs/closed/1738.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/1740.v
index ec4a7a6bc..ec4a7a6bc 100644
--- a/test-suite/bugs/closed/shouldsucceed/1740.v
+++ b/test-suite/bugs/closed/1740.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1754.v b/test-suite/bugs/closed/1754.v
index 06b8dce85..06b8dce85 100644
--- a/test-suite/bugs/closed/shouldsucceed/1754.v
+++ b/test-suite/bugs/closed/1754.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1773.v b/test-suite/bugs/closed/1773.v
index 211af89b7..211af89b7 100644
--- a/test-suite/bugs/closed/shouldsucceed/1773.v
+++ b/test-suite/bugs/closed/1773.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1774.v b/test-suite/bugs/closed/1774.v
index 4c24b481b..4c24b481b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1774.v
+++ b/test-suite/bugs/closed/1774.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/1775.v
index 932949a37..932949a37 100644
--- a/test-suite/bugs/closed/shouldsucceed/1775.v
+++ b/test-suite/bugs/closed/1775.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/1776.v
index 58491f9de..58491f9de 100644
--- a/test-suite/bugs/closed/shouldsucceed/1776.v
+++ b/test-suite/bugs/closed/1776.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1779.v b/test-suite/bugs/closed/1779.v
index 95bb66b96..95bb66b96 100644
--- a/test-suite/bugs/closed/shouldsucceed/1779.v
+++ b/test-suite/bugs/closed/1779.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/1784.v
index fb2f0ca90..fb2f0ca90 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/1784.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/1791.v
index be0e8ae8b..be0e8ae8b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1791.v
+++ b/test-suite/bugs/closed/1791.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/1834.v
index 884ac01cd..884ac01cd 100644
--- a/test-suite/bugs/closed/shouldsucceed/1834.v
+++ b/test-suite/bugs/closed/1834.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/1844.v
index 17eeb3529..17eeb3529 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/1844.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1865.v b/test-suite/bugs/closed/1865.v
index 17c199894..17c199894 100644
--- a/test-suite/bugs/closed/shouldsucceed/1865.v
+++ b/test-suite/bugs/closed/1865.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/1891.v
index 685811176..685811176 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/1891.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/1900.v
index cf03efda4..cf03efda4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1900.v
+++ b/test-suite/bugs/closed/1900.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/1901.v
index 7d86adbfb..7d86adbfb 100644
--- a/test-suite/bugs/closed/shouldsucceed/1901.v
+++ b/test-suite/bugs/closed/1901.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/1905.v
index 8c81d7510..8c81d7510 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/1905.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/1907.v
index 55fc82319..55fc82319 100644
--- a/test-suite/bugs/closed/shouldsucceed/1907.v
+++ b/test-suite/bugs/closed/1907.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/1912.v
index 987a54177..987a54177 100644
--- a/test-suite/bugs/closed/shouldsucceed/1912.v
+++ b/test-suite/bugs/closed/1912.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/1918.v
index 9d92fe12b..9d92fe12b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/1918.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/1925.v
index 4caee1c36..4caee1c36 100644
--- a/test-suite/bugs/closed/shouldsucceed/1925.v
+++ b/test-suite/bugs/closed/1925.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/1931.v
index 930ace1d5..930ace1d5 100644
--- a/test-suite/bugs/closed/shouldsucceed/1931.v
+++ b/test-suite/bugs/closed/1931.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/1935.v
index d58376198..d58376198 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/1935.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/1939.v
index 5e61529b4..5e61529b4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1939.v
+++ b/test-suite/bugs/closed/1939.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/1944.v
index ee2918c6e..ee2918c6e 100644
--- a/test-suite/bugs/closed/shouldsucceed/1944.v
+++ b/test-suite/bugs/closed/1944.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/1951.v
index 12c0ef9bf..12c0ef9bf 100644
--- a/test-suite/bugs/closed/shouldsucceed/1951.v
+++ b/test-suite/bugs/closed/1951.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/1962.v
index a6b0fee58..a6b0fee58 100644
--- a/test-suite/bugs/closed/shouldsucceed/1962.v
+++ b/test-suite/bugs/closed/1962.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/1963.v
index 11e2ee44d..11e2ee44d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1963.v
+++ b/test-suite/bugs/closed/1963.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/1977.v
index 28715040c..28715040c 100644
--- a/test-suite/bugs/closed/shouldsucceed/1977.v
+++ b/test-suite/bugs/closed/1977.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/1981.v
index 99952682d..99952682d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1981.v
+++ b/test-suite/bugs/closed/1981.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/2001.v
index d0b3bf173..d0b3bf173 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/2001.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/2017.v
index df6661483..df6661483 100644
--- a/test-suite/bugs/closed/shouldsucceed/2017.v
+++ b/test-suite/bugs/closed/2017.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/2021.v
index e598e5aed..e598e5aed 100644
--- a/test-suite/bugs/closed/shouldsucceed/2021.v
+++ b/test-suite/bugs/closed/2021.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/2027.v
index fb53c6ef4..fb53c6ef4 100644
--- a/test-suite/bugs/closed/shouldsucceed/2027.v
+++ b/test-suite/bugs/closed/2027.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/2083.v
index 5f17f7af3..5f17f7af3 100644
--- a/test-suite/bugs/closed/shouldsucceed/2083.v
+++ b/test-suite/bugs/closed/2083.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/2089.v
index aebccc942..aebccc942 100644
--- a/test-suite/bugs/closed/shouldsucceed/2089.v
+++ b/test-suite/bugs/closed/2089.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/2095.v
index 28ea99dfe..28ea99dfe 100644
--- a/test-suite/bugs/closed/shouldsucceed/2095.v
+++ b/test-suite/bugs/closed/2095.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/2108.v
index cad8baa98..cad8baa98 100644
--- a/test-suite/bugs/closed/shouldsucceed/2108.v
+++ b/test-suite/bugs/closed/2108.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/2117.v
index 6377a8b74..6377a8b74 100644
--- a/test-suite/bugs/closed/shouldsucceed/2117.v
+++ b/test-suite/bugs/closed/2117.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/2123.v
index 422a2c126..422a2c126 100644
--- a/test-suite/bugs/closed/shouldsucceed/2123.v
+++ b/test-suite/bugs/closed/2123.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/2127.v
index 142ada268..142ada268 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/2127.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/2135.v
index 61882176a..61882176a 100644
--- a/test-suite/bugs/closed/shouldsucceed/2135.v
+++ b/test-suite/bugs/closed/2135.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2136.v b/test-suite/bugs/closed/2136.v
index d2b926f37..d2b926f37 100644
--- a/test-suite/bugs/closed/shouldsucceed/2136.v
+++ b/test-suite/bugs/closed/2136.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2137.v b/test-suite/bugs/closed/2137.v
index 6c2023ab7..6c2023ab7 100644
--- a/test-suite/bugs/closed/shouldsucceed/2137.v
+++ b/test-suite/bugs/closed/2137.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/2139.v
index a7f355088..a7f355088 100644
--- a/test-suite/bugs/closed/shouldsucceed/2139.v
+++ b/test-suite/bugs/closed/2139.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/2141.v
index 941ae530f..941ae530f 100644
--- a/test-suite/bugs/closed/shouldsucceed/2141.v
+++ b/test-suite/bugs/closed/2141.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/2145.v
index 4dc0de743..4dc0de743 100644
--- a/test-suite/bugs/closed/shouldsucceed/2145.v
+++ b/test-suite/bugs/closed/2145.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/2181.v
index 62820d869..62820d869 100644
--- a/test-suite/bugs/closed/shouldsucceed/2181.v
+++ b/test-suite/bugs/closed/2181.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/2193.v
index fe2588676..fe2588676 100644
--- a/test-suite/bugs/closed/shouldsucceed/2193.v
+++ b/test-suite/bugs/closed/2193.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2230.v b/test-suite/bugs/closed/2230.v
index 5076fb2bb..5076fb2bb 100644
--- a/test-suite/bugs/closed/shouldsucceed/2230.v
+++ b/test-suite/bugs/closed/2230.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2231.v b/test-suite/bugs/closed/2231.v
index 03e2c9bbf..03e2c9bbf 100644
--- a/test-suite/bugs/closed/shouldsucceed/2231.v
+++ b/test-suite/bugs/closed/2231.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2244.v b/test-suite/bugs/closed/2244.v
index d499e515f..d499e515f 100644
--- a/test-suite/bugs/closed/shouldsucceed/2244.v
+++ b/test-suite/bugs/closed/2244.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2255.v b/test-suite/bugs/closed/2255.v
index bf80ff660..bf80ff660 100644
--- a/test-suite/bugs/closed/shouldsucceed/2255.v
+++ b/test-suite/bugs/closed/2255.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2262.v b/test-suite/bugs/closed/2262.v
index b61f18b83..b61f18b83 100644
--- a/test-suite/bugs/closed/shouldsucceed/2262.v
+++ b/test-suite/bugs/closed/2262.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/2281.v
index 40948d905..40948d905 100644
--- a/test-suite/bugs/closed/shouldsucceed/2281.v
+++ b/test-suite/bugs/closed/2281.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2295.v b/test-suite/bugs/closed/2295.v
index f5ca28dca..f5ca28dca 100644
--- a/test-suite/bugs/closed/shouldsucceed/2295.v
+++ b/test-suite/bugs/closed/2295.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2299.v b/test-suite/bugs/closed/2299.v
index c0552ca7b..c0552ca7b 100644
--- a/test-suite/bugs/closed/shouldsucceed/2299.v
+++ b/test-suite/bugs/closed/2299.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/2300.v
index 4e587cbb2..4e587cbb2 100644
--- a/test-suite/bugs/closed/shouldsucceed/2300.v
+++ b/test-suite/bugs/closed/2300.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2303.v b/test-suite/bugs/closed/2303.v
index e614b9b55..e614b9b55 100644
--- a/test-suite/bugs/closed/shouldsucceed/2303.v
+++ b/test-suite/bugs/closed/2303.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/2304.v
index 1ac2702b0..1ac2702b0 100644
--- a/test-suite/bugs/closed/shouldsucceed/2304.v
+++ b/test-suite/bugs/closed/2304.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/2307.v
index 7c0494953..7c0494953 100644
--- a/test-suite/bugs/closed/shouldsucceed/2307.v
+++ b/test-suite/bugs/closed/2307.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/2320.v
index facb9ecfc..facb9ecfc 100644
--- a/test-suite/bugs/closed/shouldsucceed/2320.v
+++ b/test-suite/bugs/closed/2320.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/2342.v
index 094e5466c..094e5466c 100644
--- a/test-suite/bugs/closed/shouldsucceed/2342.v
+++ b/test-suite/bugs/closed/2342.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2347.v b/test-suite/bugs/closed/2347.v
index e433f158e..e433f158e 100644
--- a/test-suite/bugs/closed/shouldsucceed/2347.v
+++ b/test-suite/bugs/closed/2347.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2350.v b/test-suite/bugs/closed/2350.v
index e91f22e26..e91f22e26 100644
--- a/test-suite/bugs/closed/shouldsucceed/2350.v
+++ b/test-suite/bugs/closed/2350.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2353.v b/test-suite/bugs/closed/2353.v
index baae9a6ec..baae9a6ec 100644
--- a/test-suite/bugs/closed/shouldsucceed/2353.v
+++ b/test-suite/bugs/closed/2353.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/2360.v
index 4ae97c97b..4ae97c97b 100644
--- a/test-suite/bugs/closed/shouldsucceed/2360.v
+++ b/test-suite/bugs/closed/2360.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/2362.v
index febb9c7bb..febb9c7bb 100644
--- a/test-suite/bugs/closed/shouldsucceed/2362.v
+++ b/test-suite/bugs/closed/2362.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/2375.v
index c17c426cd..c17c426cd 100644
--- a/test-suite/bugs/closed/shouldsucceed/2375.v
+++ b/test-suite/bugs/closed/2375.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/2378.v
index ab39633f8..ab39633f8 100644
--- a/test-suite/bugs/closed/shouldsucceed/2378.v
+++ b/test-suite/bugs/closed/2378.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/2388.v
index c79267119..c79267119 100644
--- a/test-suite/bugs/closed/shouldsucceed/2388.v
+++ b/test-suite/bugs/closed/2388.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/2393.v
index fb4f92619..fb4f92619 100644
--- a/test-suite/bugs/closed/shouldsucceed/2393.v
+++ b/test-suite/bugs/closed/2393.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/2404.v
index 8ac696e91..8ac696e91 100644
--- a/test-suite/bugs/closed/shouldsucceed/2404.v
+++ b/test-suite/bugs/closed/2404.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/2456.v
index 56f046c4d..56f046c4d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2456.v
+++ b/test-suite/bugs/closed/2456.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2464.v b/test-suite/bugs/closed/2464.v
index af7085872..af7085872 100644
--- a/test-suite/bugs/closed/shouldsucceed/2464.v
+++ b/test-suite/bugs/closed/2464.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/2467.v
index ad17814a8..ad17814a8 100644
--- a/test-suite/bugs/closed/shouldsucceed/2467.v
+++ b/test-suite/bugs/closed/2467.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/2473.v
index 4c3025128..4c3025128 100644
--- a/test-suite/bugs/closed/shouldsucceed/2473.v
+++ b/test-suite/bugs/closed/2473.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/2603.v
index 371bfdc57..371bfdc57 100644
--- a/test-suite/bugs/closed/shouldsucceed/2603.v
+++ b/test-suite/bugs/closed/2603.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/2608.v
index a4c95ff97..a4c95ff97 100644
--- a/test-suite/bugs/closed/shouldsucceed/2608.v
+++ b/test-suite/bugs/closed/2608.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/2613.v
index 4f0470b1d..4f0470b1d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2613.v
+++ b/test-suite/bugs/closed/2613.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/2615.v
index 54e1a07cc..54e1a07cc 100644
--- a/test-suite/bugs/closed/shouldsucceed/2615.v
+++ b/test-suite/bugs/closed/2615.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/2616.v
index 8758e32dd..8758e32dd 100644
--- a/test-suite/bugs/closed/shouldsucceed/2616.v
+++ b/test-suite/bugs/closed/2616.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/2629.v
index 759cd3dd2..759cd3dd2 100644
--- a/test-suite/bugs/closed/shouldsucceed/2629.v
+++ b/test-suite/bugs/closed/2629.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/2640.v
index da0cc68a4..da0cc68a4 100644
--- a/test-suite/bugs/closed/shouldsucceed/2640.v
+++ b/test-suite/bugs/closed/2640.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2667.v b/test-suite/bugs/closed/2667.v
index 0631e5358..0631e5358 100644
--- a/test-suite/bugs/closed/shouldsucceed/2667.v
+++ b/test-suite/bugs/closed/2667.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/2668.v
index 74c8fa347..74c8fa347 100644
--- a/test-suite/bugs/closed/shouldsucceed/2668.v
+++ b/test-suite/bugs/closed/2668.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2670.v b/test-suite/bugs/closed/2670.v
index c401420e9..c401420e9 100644
--- a/test-suite/bugs/closed/shouldsucceed/2670.v
+++ b/test-suite/bugs/closed/2670.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2680.v b/test-suite/bugs/closed/2680.v
index 0f573a289..0f573a289 100644
--- a/test-suite/bugs/closed/shouldsucceed/2680.v
+++ b/test-suite/bugs/closed/2680.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2729.v b/test-suite/bugs/closed/2729.v
index 3efca5d99..3efca5d99 100644
--- a/test-suite/bugs/closed/shouldsucceed/2729.v
+++ b/test-suite/bugs/closed/2729.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/2732.v
index f22a8cccc..f22a8cccc 100644
--- a/test-suite/bugs/closed/shouldsucceed/2732.v
+++ b/test-suite/bugs/closed/2732.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/2733.v
index 832de4f91..832de4f91 100644
--- a/test-suite/bugs/closed/shouldsucceed/2733.v
+++ b/test-suite/bugs/closed/2733.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/2734.v
index 826361be2..826361be2 100644
--- a/test-suite/bugs/closed/shouldsucceed/2734.v
+++ b/test-suite/bugs/closed/2734.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/2750.v
index fc580f101..fc580f101 100644
--- a/test-suite/bugs/closed/shouldsucceed/2750.v
+++ b/test-suite/bugs/closed/2750.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/2817.v
index 08dff9928..08dff9928 100644
--- a/test-suite/bugs/closed/shouldsucceed/2817.v
+++ b/test-suite/bugs/closed/2817.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/2836.v
index a948b75e2..a948b75e2 100644
--- a/test-suite/bugs/closed/shouldsucceed/2836.v
+++ b/test-suite/bugs/closed/2836.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2837.v b/test-suite/bugs/closed/2837.v
index 5d9844639..5d9844639 100644
--- a/test-suite/bugs/closed/shouldsucceed/2837.v
+++ b/test-suite/bugs/closed/2837.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/2928.v
index 21e92ae20..21e92ae20 100644
--- a/test-suite/bugs/closed/shouldsucceed/2928.v
+++ b/test-suite/bugs/closed/2928.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/2983.v
index 15598352b..15598352b 100644
--- a/test-suite/bugs/closed/shouldsucceed/2983.v
+++ b/test-suite/bugs/closed/2983.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/2995.v
index ba3acd088..ba3acd088 100644
--- a/test-suite/bugs/closed/shouldsucceed/2995.v
+++ b/test-suite/bugs/closed/2995.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/3000.v
index 27de34ed1..27de34ed1 100644
--- a/test-suite/bugs/closed/shouldsucceed/3000.v
+++ b/test-suite/bugs/closed/3000.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/3004.v
index 896b1958b..896b1958b 100644
--- a/test-suite/bugs/closed/shouldsucceed/3004.v
+++ b/test-suite/bugs/closed/3004.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/3008.v
index 3f3a979a3..3f3a979a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/3008.v
+++ b/test-suite/bugs/closed/3008.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3017.v b/test-suite/bugs/closed/3017.v
index 63a06bd3d..63a06bd3d 100644
--- a/test-suite/bugs/closed/shouldsucceed/3017.v
+++ b/test-suite/bugs/closed/3017.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3022.v b/test-suite/bugs/closed/3022.v
index dcfe73397..dcfe73397 100644
--- a/test-suite/bugs/closed/shouldsucceed/3022.v
+++ b/test-suite/bugs/closed/3022.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3050.v b/test-suite/bugs/closed/3050.v
index 4b1872243..4b1872243 100644
--- a/test-suite/bugs/closed/shouldsucceed/3050.v
+++ b/test-suite/bugs/closed/3050.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3054.v b/test-suite/bugs/closed/3054.v
index 936e58e19..936e58e19 100644
--- a/test-suite/bugs/closed/shouldsucceed/3054.v
+++ b/test-suite/bugs/closed/3054.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3062.v b/test-suite/bugs/closed/3062.v
index a7b5fab03..a7b5fab03 100644
--- a/test-suite/bugs/closed/shouldsucceed/3062.v
+++ b/test-suite/bugs/closed/3062.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3088.v b/test-suite/bugs/closed/3088.v
index 3c362510e..3c362510e 100644
--- a/test-suite/bugs/closed/shouldsucceed/3088.v
+++ b/test-suite/bugs/closed/3088.v
diff --git a/test-suite/bugs/closed/shouldsucceed/3093.v b/test-suite/bugs/closed/3093.v
index f6b4a03f3..f6b4a03f3 100644
--- a/test-suite/bugs/closed/shouldsucceed/3093.v
+++ b/test-suite/bugs/closed/3093.v
diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/335.v
index 166fa7a9f..166fa7a9f 100644
--- a/test-suite/bugs/closed/shouldsucceed/335.v
+++ b/test-suite/bugs/closed/335.v
diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/348.v
index 28cc5cb1e..28cc5cb1e 100644
--- a/test-suite/bugs/closed/shouldsucceed/348.v
+++ b/test-suite/bugs/closed/348.v
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/38.v
index 4fc8d7c97..4fc8d7c97 100644
--- a/test-suite/bugs/closed/shouldsucceed/38.v
+++ b/test-suite/bugs/closed/38.v
diff --git a/test-suite/bugs/closed/shouldsucceed/545.v b/test-suite/bugs/closed/545.v
index 926af7dd1..926af7dd1 100644
--- a/test-suite/bugs/closed/shouldsucceed/545.v
+++ b/test-suite/bugs/closed/545.v
diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/808_2411.v
index 1c13e7454..1c13e7454 100644
--- a/test-suite/bugs/closed/shouldsucceed/808_2411.v
+++ b/test-suite/bugs/closed/808_2411.v
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/846.v
index ee5ec1fa6..ee5ec1fa6 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/846.v
diff --git a/test-suite/bugs/closed/shouldsucceed/931.v b/test-suite/bugs/closed/931.v
index 21f15e721..21f15e721 100644
--- a/test-suite/bugs/closed/shouldsucceed/931.v
+++ b/test-suite/bugs/closed/931.v
diff --git a/test-suite/bugs/closed/shouldsucceed/1519.v b/test-suite/bugs/closed/shouldsucceed/1519.v
deleted file mode 100644
index 66bab241d..000000000
--- a/test-suite/bugs/closed/shouldsucceed/1519.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Section S.
-
-  Variable A:Prop.
-  Variable W:A.
-
-  Remark T: A -> A.
-    intro Z.
-    rename W into Z_.
-    rename Z into W.
-    rename Z_ into Z.
-    exact Z.
-  Qed.
-
-End S.