diff options
author | 2013-09-20 12:40:28 +0000 | |
---|---|---|
committer | 2013-09-20 12:40:28 +0000 | |
commit | e46ce40cee2c34f47acb55d2b24bd09f00987556 (patch) | |
tree | 696da31b3041d1b7c69244ab5a48f77b87ccf79b | |
parent | 20bb249ed0e19cc0132519e3de06fafe2ba500c3 (diff) |
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
-rw-r--r-- | test-suite/bugs/closed/1041.v (renamed from test-suite/bugs/closed/shouldsucceed/1041.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1100.v (renamed from test-suite/bugs/closed/shouldsucceed/1100.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/121.v (renamed from test-suite/bugs/closed/shouldsucceed/121.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1243.v (renamed from test-suite/bugs/closed/shouldsucceed/1243.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1302.v (renamed from test-suite/bugs/closed/shouldsucceed/1302.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1322.v (renamed from test-suite/bugs/closed/shouldsucceed/1322.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1411.v (renamed from test-suite/bugs/closed/shouldsucceed/1411.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1414.v (renamed from test-suite/bugs/closed/shouldsucceed/1414.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1416.v (renamed from test-suite/bugs/closed/shouldsucceed/1416.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1419.v (renamed from test-suite/bugs/closed/shouldsucceed/1419.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1425.v (renamed from test-suite/bugs/closed/shouldsucceed/1425.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1446.v (renamed from test-suite/bugs/closed/shouldsucceed/1446.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1448.v (renamed from test-suite/bugs/closed/shouldsucceed/1448.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1477.v (renamed from test-suite/bugs/closed/shouldsucceed/1477.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1483.v (renamed from test-suite/bugs/closed/shouldsucceed/1483.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1507.v (renamed from test-suite/bugs/closed/shouldsucceed/1507.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1568.v (renamed from test-suite/bugs/closed/shouldsucceed/1568.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1576.v (renamed from test-suite/bugs/closed/shouldsucceed/1576.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1582.v (renamed from test-suite/bugs/closed/shouldsucceed/1582.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1604.v (renamed from test-suite/bugs/closed/shouldsucceed/1604.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1614.v (renamed from test-suite/bugs/closed/shouldsucceed/1614.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1618.v (renamed from test-suite/bugs/closed/shouldsucceed/1618.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1634.v (renamed from test-suite/bugs/closed/shouldsucceed/1634.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1643.v (renamed from test-suite/bugs/closed/shouldsucceed/1643.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1680.v (renamed from test-suite/bugs/closed/shouldsucceed/1680.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1683.v (renamed from test-suite/bugs/closed/shouldsucceed/1683.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1696.v (renamed from test-suite/bugs/closed/shouldsucceed/1696.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1704.v (renamed from test-suite/bugs/closed/shouldsucceed/1704.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1711.v (renamed from test-suite/bugs/closed/shouldsucceed/1711.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1718.v (renamed from test-suite/bugs/closed/shouldsucceed/1718.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1738.v (renamed from test-suite/bugs/closed/shouldsucceed/1738.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1740.v (renamed from test-suite/bugs/closed/shouldsucceed/1740.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1754.v (renamed from test-suite/bugs/closed/shouldsucceed/1754.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1773.v (renamed from test-suite/bugs/closed/shouldsucceed/1773.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1774.v (renamed from test-suite/bugs/closed/shouldsucceed/1774.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1775.v (renamed from test-suite/bugs/closed/shouldsucceed/1775.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1776.v (renamed from test-suite/bugs/closed/shouldsucceed/1776.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1779.v (renamed from test-suite/bugs/closed/shouldsucceed/1779.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1784.v (renamed from test-suite/bugs/closed/shouldsucceed/1784.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1791.v (renamed from test-suite/bugs/closed/shouldsucceed/1791.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1834.v (renamed from test-suite/bugs/closed/shouldsucceed/1834.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1844.v (renamed from test-suite/bugs/closed/shouldsucceed/1844.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1865.v (renamed from test-suite/bugs/closed/shouldsucceed/1865.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1891.v (renamed from test-suite/bugs/closed/shouldsucceed/1891.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1900.v (renamed from test-suite/bugs/closed/shouldsucceed/1900.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1901.v (renamed from test-suite/bugs/closed/shouldsucceed/1901.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1905.v (renamed from test-suite/bugs/closed/shouldsucceed/1905.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1907.v (renamed from test-suite/bugs/closed/shouldsucceed/1907.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1912.v (renamed from test-suite/bugs/closed/shouldsucceed/1912.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1918.v (renamed from test-suite/bugs/closed/shouldsucceed/1918.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1925.v (renamed from test-suite/bugs/closed/shouldsucceed/1925.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1931.v (renamed from test-suite/bugs/closed/shouldsucceed/1931.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1935.v (renamed from test-suite/bugs/closed/shouldsucceed/1935.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1939.v (renamed from test-suite/bugs/closed/shouldsucceed/1939.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1944.v (renamed from test-suite/bugs/closed/shouldsucceed/1944.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1951.v (renamed from test-suite/bugs/closed/shouldsucceed/1951.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1962.v (renamed from test-suite/bugs/closed/shouldsucceed/1962.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1963.v (renamed from test-suite/bugs/closed/shouldsucceed/1963.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1977.v (renamed from test-suite/bugs/closed/shouldsucceed/1977.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/1981.v (renamed from test-suite/bugs/closed/shouldsucceed/1981.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2001.v (renamed from test-suite/bugs/closed/shouldsucceed/2001.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2017.v (renamed from test-suite/bugs/closed/shouldsucceed/2017.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2021.v (renamed from test-suite/bugs/closed/shouldsucceed/2021.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2027.v (renamed from test-suite/bugs/closed/shouldsucceed/2027.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2083.v (renamed from test-suite/bugs/closed/shouldsucceed/2083.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2089.v (renamed from test-suite/bugs/closed/shouldsucceed/2089.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2095.v (renamed from test-suite/bugs/closed/shouldsucceed/2095.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2108.v (renamed from test-suite/bugs/closed/shouldsucceed/2108.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2117.v (renamed from test-suite/bugs/closed/shouldsucceed/2117.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2123.v (renamed from test-suite/bugs/closed/shouldsucceed/2123.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2127.v (renamed from test-suite/bugs/closed/shouldsucceed/2127.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2135.v (renamed from test-suite/bugs/closed/shouldsucceed/2135.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2136.v (renamed from test-suite/bugs/closed/shouldsucceed/2136.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2137.v (renamed from test-suite/bugs/closed/shouldsucceed/2137.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2139.v (renamed from test-suite/bugs/closed/shouldsucceed/2139.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2141.v (renamed from test-suite/bugs/closed/shouldsucceed/2141.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2145.v (renamed from test-suite/bugs/closed/shouldsucceed/2145.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2181.v (renamed from test-suite/bugs/closed/shouldsucceed/2181.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2193.v (renamed from test-suite/bugs/closed/shouldsucceed/2193.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2230.v (renamed from test-suite/bugs/closed/shouldsucceed/2230.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2231.v (renamed from test-suite/bugs/closed/shouldsucceed/2231.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2244.v (renamed from test-suite/bugs/closed/shouldsucceed/2244.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2255.v (renamed from test-suite/bugs/closed/shouldsucceed/2255.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2262.v (renamed from test-suite/bugs/closed/shouldsucceed/2262.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2281.v (renamed from test-suite/bugs/closed/shouldsucceed/2281.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2295.v (renamed from test-suite/bugs/closed/shouldsucceed/2295.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2299.v (renamed from test-suite/bugs/closed/shouldsucceed/2299.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2300.v (renamed from test-suite/bugs/closed/shouldsucceed/2300.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2303.v (renamed from test-suite/bugs/closed/shouldsucceed/2303.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2304.v (renamed from test-suite/bugs/closed/shouldsucceed/2304.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2307.v (renamed from test-suite/bugs/closed/shouldsucceed/2307.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2320.v (renamed from test-suite/bugs/closed/shouldsucceed/2320.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2342.v (renamed from test-suite/bugs/closed/shouldsucceed/2342.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2347.v (renamed from test-suite/bugs/closed/shouldsucceed/2347.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2350.v (renamed from test-suite/bugs/closed/shouldsucceed/2350.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2353.v (renamed from test-suite/bugs/closed/shouldsucceed/2353.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2360.v (renamed from test-suite/bugs/closed/shouldsucceed/2360.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2362.v (renamed from test-suite/bugs/closed/shouldsucceed/2362.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2375.v (renamed from test-suite/bugs/closed/shouldsucceed/2375.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2378.v (renamed from test-suite/bugs/closed/shouldsucceed/2378.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2388.v (renamed from test-suite/bugs/closed/shouldsucceed/2388.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2393.v (renamed from test-suite/bugs/closed/shouldsucceed/2393.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2404.v (renamed from test-suite/bugs/closed/shouldsucceed/2404.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2456.v (renamed from test-suite/bugs/closed/shouldsucceed/2456.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2464.v (renamed from test-suite/bugs/closed/shouldsucceed/2464.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2467.v (renamed from test-suite/bugs/closed/shouldsucceed/2467.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2473.v (renamed from test-suite/bugs/closed/shouldsucceed/2473.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2603.v (renamed from test-suite/bugs/closed/shouldsucceed/2603.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2608.v (renamed from test-suite/bugs/closed/shouldsucceed/2608.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2613.v (renamed from test-suite/bugs/closed/shouldsucceed/2613.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2615.v (renamed from test-suite/bugs/closed/shouldsucceed/2615.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2616.v (renamed from test-suite/bugs/closed/shouldsucceed/2616.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2629.v (renamed from test-suite/bugs/closed/shouldsucceed/2629.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2640.v (renamed from test-suite/bugs/closed/shouldsucceed/2640.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2667.v (renamed from test-suite/bugs/closed/shouldsucceed/2667.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2668.v (renamed from test-suite/bugs/closed/shouldsucceed/2668.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2670.v (renamed from test-suite/bugs/closed/shouldsucceed/2670.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2680.v (renamed from test-suite/bugs/closed/shouldsucceed/2680.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2729.v (renamed from test-suite/bugs/closed/shouldsucceed/2729.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2732.v (renamed from test-suite/bugs/closed/shouldsucceed/2732.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2733.v (renamed from test-suite/bugs/closed/shouldsucceed/2733.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2734.v (renamed from test-suite/bugs/closed/shouldsucceed/2734.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2750.v (renamed from test-suite/bugs/closed/shouldsucceed/2750.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2817.v (renamed from test-suite/bugs/closed/shouldsucceed/2817.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2836.v (renamed from test-suite/bugs/closed/shouldsucceed/2836.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2837.v (renamed from test-suite/bugs/closed/shouldsucceed/2837.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2928.v (renamed from test-suite/bugs/closed/shouldsucceed/2928.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2983.v (renamed from test-suite/bugs/closed/shouldsucceed/2983.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2995.v (renamed from test-suite/bugs/closed/shouldsucceed/2995.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3000.v (renamed from test-suite/bugs/closed/shouldsucceed/3000.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3004.v (renamed from test-suite/bugs/closed/shouldsucceed/3004.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3008.v (renamed from test-suite/bugs/closed/shouldsucceed/3008.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3017.v (renamed from test-suite/bugs/closed/shouldsucceed/3017.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3022.v (renamed from test-suite/bugs/closed/shouldsucceed/3022.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3050.v (renamed from test-suite/bugs/closed/shouldsucceed/3050.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3054.v (renamed from test-suite/bugs/closed/shouldsucceed/3054.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3062.v (renamed from test-suite/bugs/closed/shouldsucceed/3062.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3088.v (renamed from test-suite/bugs/closed/shouldsucceed/3088.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/3093.v (renamed from test-suite/bugs/closed/shouldsucceed/3093.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/335.v (renamed from test-suite/bugs/closed/shouldsucceed/335.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/348.v (renamed from test-suite/bugs/closed/shouldsucceed/348.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/38.v (renamed from test-suite/bugs/closed/shouldsucceed/38.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/545.v (renamed from test-suite/bugs/closed/shouldsucceed/545.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/808_2411.v (renamed from test-suite/bugs/closed/shouldsucceed/808_2411.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/846.v (renamed from test-suite/bugs/closed/shouldsucceed/846.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/931.v (renamed from test-suite/bugs/closed/shouldsucceed/931.v) | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1519.v | 14 |
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. |