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 a5de82e0d8..a5de82e0d8 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 32c78b4b9e..32c78b4b9e 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 8c5a38859f..8c5a38859f 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 7d6781db27..7d6781db27 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 e94dfcfb05..e94dfcfb05 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 1ec7d452a6..1ec7d452a6 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 a1a7b288a5..a1a7b288a5 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 ee9e2504a6..ee9e2504a6 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 ee09200573..ee09200573 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 d021107d1d..d021107d1d 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 6be30174ae..6be30174ae 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 8cb2d653b6..8cb2d653b6 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 fe3b4c8b41..fe3b4c8b41 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 dfc8c32806..dfc8c32806 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 a3d7f16830..a3d7f16830 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 f2ab910034..f2ab910034 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 3609e9c83b..3609e9c83b 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 3621f7a1ff..3621f7a1ff 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 be5d3dd211..be5d3dd211 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 22c3df824b..22c3df824b 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 6bc165d406..6bc165d406 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 a9b067ceb2..a9b067ceb2 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 0150c25038..0150c25038 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 879a65b183..879a65b183 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 524c7bab42..524c7bab42 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 3e99694b3c..3e99694b3c 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 0826428a34..0826428a34 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 4b02d5f93b..4b02d5f93b 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 e16612e380..e16612e380 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 715fa94199..715fa94199 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 c2926a2b25..c2926a2b25 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 ec4a7a6bcb..ec4a7a6bcb 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 06b8dce851..06b8dce851 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 211af89b70..211af89b70 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 4c24b481bd..4c24b481bd 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 932949a371..932949a371 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 58491f9de1..58491f9de1 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 95bb66b962..95bb66b962 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 fb2f0ca90e..fb2f0ca90e 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 be0e8ae8ba..be0e8ae8ba 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 884ac01cd2..884ac01cd2 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 17eeb35291..17eeb35291 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 17c1998948..17c1998948 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 685811176a..685811176a 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 cf03efda42..cf03efda42 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 7d86adbfb2..7d86adbfb2 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 8c81d7510b..8c81d7510b 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 55fc823190..55fc823190 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 987a541778..987a541778 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 9d92fe12b8..9d92fe12b8 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 4caee1c36d..4caee1c36d 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 930ace1d55..930ace1d55 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 d583761985..d583761985 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 5e61529b4b..5e61529b4b 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 ee2918c6e9..ee2918c6e9 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 12c0ef9bf5..12c0ef9bf5 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 a6b0fee584..a6b0fee584 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 11e2ee44d6..11e2ee44d6 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 28715040ce..28715040ce 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 99952682d5..99952682d5 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 d0b3bf1732..d0b3bf1732 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 df6661483a..df6661483a 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 e598e5aed7..e598e5aed7 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 fb53c6ef43..fb53c6ef43 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 5f17f7af35..5f17f7af35 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 aebccc9424..aebccc9424 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 28ea99dfef..28ea99dfef 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 cad8baa981..cad8baa981 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 6377a8b74a..6377a8b74a 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 422a2c126e..422a2c126e 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 142ada268b..142ada268b 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 61882176aa..61882176aa 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 d2b926f379..d2b926f379 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 6c2023ab7b..6c2023ab7b 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 a7f3550888..a7f3550888 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 941ae530fd..941ae530fd 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 4dc0de7433..4dc0de7433 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 62820d8699..62820d8699 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 fe2588676d..fe2588676d 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 5076fb2bb7..5076fb2bb7 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 03e2c9bbf4..03e2c9bbf4 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 d499e515fe..d499e515fe 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 bf80ff6607..bf80ff6607 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 b61f18b837..b61f18b837 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 40948d9059..40948d9059 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 f5ca28dcaa..f5ca28dcaa 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 c0552ca7b3..c0552ca7b3 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 4e587cbb25..4e587cbb25 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 e614b9b552..e614b9b552 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 1ac2702b0a..1ac2702b0a 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 7c04949539..7c04949539 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 facb9ecfc9..facb9ecfc9 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 094e5466cb..094e5466cb 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 e433f158e4..e433f158e4 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 e91f22e267..e91f22e267 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 baae9a6ece..baae9a6ece 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 4ae97c97bb..4ae97c97bb 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 febb9c7bb0..febb9c7bb0 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 c17c426cda..c17c426cda 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 ab39633f87..ab39633f87 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 c792671193..c792671193 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 fb4f92619f..fb4f92619f 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 8ac696e912..8ac696e912 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 56f046c4d7..56f046c4d7 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 af70858720..af70858720 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 ad17814a8f..ad17814a8f 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 4c3025128c..4c3025128c 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 371bfdc575..371bfdc575 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 a4c95ff97c..a4c95ff97c 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 4f0470b1df..4f0470b1df 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 54e1a07cc8..54e1a07cc8 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 8758e32dd8..8758e32dd8 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 759cd3dd28..759cd3dd28 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 da0cc68a4e..da0cc68a4e 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 0631e5358d..0631e5358d 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 74c8fa347b..74c8fa347b 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 c401420e94..c401420e94 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 0f573a2898..0f573a2898 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 3efca5d993..3efca5d993 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 f22a8cccc5..f22a8cccc5 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 832de4f913..832de4f913 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 826361be2b..826361be2b 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 fc580f1018..fc580f1018 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 08dff99287..08dff99287 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 a948b75e27..a948b75e27 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 5d98446395..5d98446395 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 21e92ae20c..21e92ae20c 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 15598352b1..15598352b1 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 ba3acd088d..ba3acd088d 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 27de34ed17..27de34ed17 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 896b1958b0..896b1958b0 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 3f3a979a35..3f3a979a35 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 63a06bd3d6..63a06bd3d6 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 dcfe733974..dcfe733974 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 4b18722431..4b18722431 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 936e58e197..936e58e197 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 a7b5fab03e..a7b5fab03e 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 3c362510e3..3c362510e3 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 f6b4a03f3b..f6b4a03f3b 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 166fa7a9f2..166fa7a9f2 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 28cc5cb1e6..28cc5cb1e6 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 4fc8d7c97d..4fc8d7c97d 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 926af7dd1c..926af7dd1c 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 1c13e74547..1c13e74547 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 ee5ec1fa6a..ee5ec1fa6a 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 21f15e7218..21f15e7218 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 66bab241d8..0000000000
--- 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.