aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-17 17:18:39 +0200
committerMatthieu Sozeau2014-06-17 17:19:04 +0200
commit35d92d68c0b2123a3994a90ef7e2b8cbb946f041 (patch)
tree228215b848782c480437ac588b594bf7334e7669
parent83dff8025ae4cf919ea92d39e4619e72fe9b3f42 (diff)
Not a bug, keep for backwards compatibility
-rw-r--r--test-suite/bugs/closed/HoTT_coq_103.v (renamed from test-suite/bugs/opened/HoTT_coq_103.v)0
1 files changed, 0 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_103.v b/test-suite/bugs/closed/HoTT_coq_103.v
index 7ecf7671e5..7ecf7671e5 100644
--- a/test-suite/bugs/opened/HoTT_coq_103.v
+++ b/test-suite/bugs/closed/HoTT_coq_103.v