diff options
| -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 265310b1a..265310b1a 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 9c360c9f4..9c360c9f4 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 1fd7e251f..1fd7e251f 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 6747d6af2..6747d6af2 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 8132f51d2..8132f51d2 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 85a2714c7..85a2714c7 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 c9d8fe137..c9d8fe137 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 39a7103d1..39a7103d1 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 c4dbf74cd..c4dbf74cd 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 9697928ff..9697928ff 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 b06830dd0..b06830dd0 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 590bdd157..590bdd157 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 dac575b54..dac575b54 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 a14fb6aa5..a14fb6aa5 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 f79fe1c1e..f79fe1c1e 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 d1ea16ec3..d1ea16ec3 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 6c0221479..6c0221479 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 1c584d295..1c584d295 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 fae954f81..fae954f81 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 6c02cad56..6c02cad56 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 36f478002..36f478002 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 6de3ebdbd..6de3ebdbd 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 03886695c..03886695c 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 494b25c7b..494b25c7b 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 d007e4e23..d007e4e23 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 041c67997..041c67997 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 54ae4704a..54ae4704a 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 1e7be20d5..1e7be20d5 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 9c89a6ab9..9c89a6ab9 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 72b4ffe94..72b4ffe94 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 7b1dc8dea..7b1dc8dea 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 5bb7fa8c1..5bb7fa8c1 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 86001d26e..86001d26e 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 d3ef9f58c..d3ef9f58c 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 c3a83627e..c3a83627e 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 5ec40dbcb..5ec40dbcb 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 56feadb40..56feadb40 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 3ef531bc9..3ef531bc9 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 c1e133eeb..c1e133eeb 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 7a0494911..7a0494911 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 1ba8e5c34..1ba8e5c34 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 e6e90ada8..e6e90ada8 100644 --- a/test-suite/bugs/closed/HoTT_coq_124.v +++ b/test-suite/bugs/opened/HoTT_coq_124.v |