aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross2014-05-09 10:13:32 -0400
committerMatthieu Sozeau2014-05-10 15:39:39 +0200
commitc7284415e4bdd3315c84c7d15d140d3fee000bc5 (patch)
treecc8ded3feba7e1da0dd4f7d17b7e5f974de752c3
parent3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (diff)
Move opened bugs to bugs/opened
-rw-r--r--test-suite/bugs/opened/3230.v (renamed from test-suite/bugs/closed/3230.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_007.v (renamed from test-suite/bugs/closed/HoTT_coq_007.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_014.v (renamed from test-suite/bugs/closed/HoTT_coq_014.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_020.v (renamed from test-suite/bugs/closed/HoTT_coq_020.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_027.v (renamed from test-suite/bugs/closed/HoTT_coq_027.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_029.v (renamed from test-suite/bugs/closed/HoTT_coq_029.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_030.v (renamed from test-suite/bugs/closed/HoTT_coq_030.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_032.v (renamed from test-suite/bugs/closed/HoTT_coq_032.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_033.v (renamed from test-suite/bugs/closed/HoTT_coq_033.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_034.v (renamed from test-suite/bugs/closed/HoTT_coq_034.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_036.v (renamed from test-suite/bugs/closed/HoTT_coq_036.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_045.v (renamed from test-suite/bugs/closed/HoTT_coq_045.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_052.v (renamed from test-suite/bugs/closed/HoTT_coq_052.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_053.v (renamed from test-suite/bugs/closed/HoTT_coq_053.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_054.v (renamed from test-suite/bugs/closed/HoTT_coq_054.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_061.v (renamed from test-suite/bugs/closed/HoTT_coq_061.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_062.v (renamed from test-suite/bugs/closed/HoTT_coq_062.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_063.v (renamed from test-suite/bugs/closed/HoTT_coq_063.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_064.v (renamed from test-suite/bugs/closed/HoTT_coq_064.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_078.v (renamed from test-suite/bugs/closed/HoTT_coq_078.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_080.v (renamed from test-suite/bugs/closed/HoTT_coq_080.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_081.v (renamed from test-suite/bugs/closed/HoTT_coq_081.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_082.v (renamed from test-suite/bugs/closed/HoTT_coq_082.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_083.v (renamed from test-suite/bugs/closed/HoTT_coq_083.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_084.v (renamed from test-suite/bugs/closed/HoTT_coq_084.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_085.v (renamed from test-suite/bugs/closed/HoTT_coq_085.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_089.v (renamed from test-suite/bugs/closed/HoTT_coq_089.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_098.v (renamed from test-suite/bugs/closed/HoTT_coq_098.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_101.v (renamed from test-suite/bugs/closed/HoTT_coq_101.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_102.v (renamed from test-suite/bugs/closed/HoTT_coq_102.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_103.v (renamed from test-suite/bugs/closed/HoTT_coq_103.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_104.v (renamed from test-suite/bugs/closed/HoTT_coq_104.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_105.v (renamed from test-suite/bugs/closed/HoTT_coq_105.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_106.v (renamed from test-suite/bugs/closed/HoTT_coq_106.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_107.v (renamed from test-suite/bugs/closed/HoTT_coq_107.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_110.v (renamed from test-suite/bugs/closed/HoTT_coq_110.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_111.v (renamed from test-suite/bugs/closed/HoTT_coq_111.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_113.v (renamed from test-suite/bugs/closed/HoTT_coq_113.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_115.v (renamed from test-suite/bugs/closed/HoTT_coq_115.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_120.v (renamed from test-suite/bugs/closed/HoTT_coq_120.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_122.v (renamed from test-suite/bugs/closed/HoTT_coq_122.v)0
-rw-r--r--test-suite/bugs/opened/HoTT_coq_124.v (renamed from test-suite/bugs/closed/HoTT_coq_124.v)0
42 files changed, 0 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3230.v b/test-suite/bugs/opened/3230.v
index 265310b1a3..265310b1a3 100644
--- a/test-suite/bugs/closed/3230.v
+++ b/test-suite/bugs/opened/3230.v
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
index 9c360c9f4e..9c360c9f4e 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/opened/HoTT_coq_007.v
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/opened/HoTT_coq_014.v
index 1fd7e251f4..1fd7e251f4 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/opened/HoTT_coq_014.v
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/opened/HoTT_coq_020.v
index 6747d6af22..6747d6af22 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/opened/HoTT_coq_020.v
diff --git a/test-suite/bugs/closed/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index 8132f51d2d..8132f51d2d 100644
--- a/test-suite/bugs/closed/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
diff --git a/test-suite/bugs/closed/HoTT_coq_029.v b/test-suite/bugs/opened/HoTT_coq_029.v
index 85a2714c7a..85a2714c7a 100644
--- a/test-suite/bugs/closed/HoTT_coq_029.v
+++ b/test-suite/bugs/opened/HoTT_coq_029.v
diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/opened/HoTT_coq_030.v
index c9d8fe137e..c9d8fe137e 100644
--- a/test-suite/bugs/closed/HoTT_coq_030.v
+++ b/test-suite/bugs/opened/HoTT_coq_030.v
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/opened/HoTT_coq_032.v
index 39a7103d1b..39a7103d1b 100644
--- a/test-suite/bugs/closed/HoTT_coq_032.v
+++ b/test-suite/bugs/opened/HoTT_coq_032.v
diff --git a/test-suite/bugs/closed/HoTT_coq_033.v b/test-suite/bugs/opened/HoTT_coq_033.v
index c4dbf74cd2..c4dbf74cd2 100644
--- a/test-suite/bugs/closed/HoTT_coq_033.v
+++ b/test-suite/bugs/opened/HoTT_coq_033.v
diff --git a/test-suite/bugs/closed/HoTT_coq_034.v b/test-suite/bugs/opened/HoTT_coq_034.v
index 9697928ffa..9697928ffa 100644
--- a/test-suite/bugs/closed/HoTT_coq_034.v
+++ b/test-suite/bugs/opened/HoTT_coq_034.v
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/opened/HoTT_coq_036.v
index b06830dd0a..b06830dd0a 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/opened/HoTT_coq_036.v
diff --git a/test-suite/bugs/closed/HoTT_coq_045.v b/test-suite/bugs/opened/HoTT_coq_045.v
index 590bdd1571..590bdd1571 100644
--- a/test-suite/bugs/closed/HoTT_coq_045.v
+++ b/test-suite/bugs/opened/HoTT_coq_045.v
diff --git a/test-suite/bugs/closed/HoTT_coq_052.v b/test-suite/bugs/opened/HoTT_coq_052.v
index dac575b541..dac575b541 100644
--- a/test-suite/bugs/closed/HoTT_coq_052.v
+++ b/test-suite/bugs/opened/HoTT_coq_052.v
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/opened/HoTT_coq_053.v
index a14fb6aa57..a14fb6aa57 100644
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ b/test-suite/bugs/opened/HoTT_coq_053.v
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/opened/HoTT_coq_054.v
index f79fe1c1e7..f79fe1c1e7 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/opened/HoTT_coq_054.v
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/opened/HoTT_coq_061.v
index d1ea16ec33..d1ea16ec33 100644
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ b/test-suite/bugs/opened/HoTT_coq_061.v
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index 6c02214795..6c02214795 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
diff --git a/test-suite/bugs/closed/HoTT_coq_063.v b/test-suite/bugs/opened/HoTT_coq_063.v
index 1c584d2954..1c584d2954 100644
--- a/test-suite/bugs/closed/HoTT_coq_063.v
+++ b/test-suite/bugs/opened/HoTT_coq_063.v
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/opened/HoTT_coq_064.v
index fae954f81a..fae954f81a 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/opened/HoTT_coq_064.v
diff --git a/test-suite/bugs/closed/HoTT_coq_078.v b/test-suite/bugs/opened/HoTT_coq_078.v
index 6c02cad567..6c02cad567 100644
--- a/test-suite/bugs/closed/HoTT_coq_078.v
+++ b/test-suite/bugs/opened/HoTT_coq_078.v
diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/opened/HoTT_coq_080.v
index 36f4780029..36f4780029 100644
--- a/test-suite/bugs/closed/HoTT_coq_080.v
+++ b/test-suite/bugs/opened/HoTT_coq_080.v
diff --git a/test-suite/bugs/closed/HoTT_coq_081.v b/test-suite/bugs/opened/HoTT_coq_081.v
index 6de3ebdbd4..6de3ebdbd4 100644
--- a/test-suite/bugs/closed/HoTT_coq_081.v
+++ b/test-suite/bugs/opened/HoTT_coq_081.v
diff --git a/test-suite/bugs/closed/HoTT_coq_082.v b/test-suite/bugs/opened/HoTT_coq_082.v
index 03886695cf..03886695cf 100644
--- a/test-suite/bugs/closed/HoTT_coq_082.v
+++ b/test-suite/bugs/opened/HoTT_coq_082.v
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
index 494b25c7b1..494b25c7b1 100644
--- a/test-suite/bugs/closed/HoTT_coq_083.v
+++ b/test-suite/bugs/opened/HoTT_coq_083.v
diff --git a/test-suite/bugs/closed/HoTT_coq_084.v b/test-suite/bugs/opened/HoTT_coq_084.v
index d007e4e235..d007e4e235 100644
--- a/test-suite/bugs/closed/HoTT_coq_084.v
+++ b/test-suite/bugs/opened/HoTT_coq_084.v
diff --git a/test-suite/bugs/closed/HoTT_coq_085.v b/test-suite/bugs/opened/HoTT_coq_085.v
index 041c67997f..041c67997f 100644
--- a/test-suite/bugs/closed/HoTT_coq_085.v
+++ b/test-suite/bugs/opened/HoTT_coq_085.v
diff --git a/test-suite/bugs/closed/HoTT_coq_089.v b/test-suite/bugs/opened/HoTT_coq_089.v
index 54ae4704af..54ae4704af 100644
--- a/test-suite/bugs/closed/HoTT_coq_089.v
+++ b/test-suite/bugs/opened/HoTT_coq_089.v
diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/opened/HoTT_coq_098.v
index 1e7be20d5f..1e7be20d5f 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/opened/HoTT_coq_098.v
diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/opened/HoTT_coq_101.v
index 9c89a6ab9d..9c89a6ab9d 100644
--- a/test-suite/bugs/closed/HoTT_coq_101.v
+++ b/test-suite/bugs/opened/HoTT_coq_101.v
diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/opened/HoTT_coq_102.v
index 72b4ffe94e..72b4ffe94e 100644
--- a/test-suite/bugs/closed/HoTT_coq_102.v
+++ b/test-suite/bugs/opened/HoTT_coq_102.v
diff --git a/test-suite/bugs/closed/HoTT_coq_103.v b/test-suite/bugs/opened/HoTT_coq_103.v
index 7b1dc8deab..7b1dc8deab 100644
--- a/test-suite/bugs/closed/HoTT_coq_103.v
+++ b/test-suite/bugs/opened/HoTT_coq_103.v
diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/opened/HoTT_coq_104.v
index 5bb7fa8c12..5bb7fa8c12 100644
--- a/test-suite/bugs/closed/HoTT_coq_104.v
+++ b/test-suite/bugs/opened/HoTT_coq_104.v
diff --git a/test-suite/bugs/closed/HoTT_coq_105.v b/test-suite/bugs/opened/HoTT_coq_105.v
index 86001d26eb..86001d26eb 100644
--- a/test-suite/bugs/closed/HoTT_coq_105.v
+++ b/test-suite/bugs/opened/HoTT_coq_105.v
diff --git a/test-suite/bugs/closed/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v
index d3ef9f58c3..d3ef9f58c3 100644
--- a/test-suite/bugs/closed/HoTT_coq_106.v
+++ b/test-suite/bugs/opened/HoTT_coq_106.v
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/opened/HoTT_coq_107.v
index c3a83627ee..c3a83627ee 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/opened/HoTT_coq_107.v
diff --git a/test-suite/bugs/closed/HoTT_coq_110.v b/test-suite/bugs/opened/HoTT_coq_110.v
index 5ec40dbcb9..5ec40dbcb9 100644
--- a/test-suite/bugs/closed/HoTT_coq_110.v
+++ b/test-suite/bugs/opened/HoTT_coq_110.v
diff --git a/test-suite/bugs/closed/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v
index 56feadb403..56feadb403 100644
--- a/test-suite/bugs/closed/HoTT_coq_111.v
+++ b/test-suite/bugs/opened/HoTT_coq_111.v
diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/opened/HoTT_coq_113.v
index 3ef531bc96..3ef531bc96 100644
--- a/test-suite/bugs/closed/HoTT_coq_113.v
+++ b/test-suite/bugs/opened/HoTT_coq_113.v
diff --git a/test-suite/bugs/closed/HoTT_coq_115.v b/test-suite/bugs/opened/HoTT_coq_115.v
index c1e133eeb2..c1e133eeb2 100644
--- a/test-suite/bugs/closed/HoTT_coq_115.v
+++ b/test-suite/bugs/opened/HoTT_coq_115.v
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7a04949114..7a04949114 100644
--- a/test-suite/bugs/closed/HoTT_coq_120.v
+++ b/test-suite/bugs/opened/HoTT_coq_120.v
diff --git a/test-suite/bugs/closed/HoTT_coq_122.v b/test-suite/bugs/opened/HoTT_coq_122.v
index 1ba8e5c345..1ba8e5c345 100644
--- a/test-suite/bugs/closed/HoTT_coq_122.v
+++ b/test-suite/bugs/opened/HoTT_coq_122.v
diff --git a/test-suite/bugs/closed/HoTT_coq_124.v b/test-suite/bugs/opened/HoTT_coq_124.v
index e6e90ada81..e6e90ada81 100644
--- a/test-suite/bugs/closed/HoTT_coq_124.v
+++ b/test-suite/bugs/opened/HoTT_coq_124.v