aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
diff options
context:
space:
mode:
authorVincent Laporte2018-10-02 13:44:46 +0000
committerVincent Laporte2018-10-04 08:01:34 +0000
commitdb22ae6140259dd065fdd80af4cb3c3bab41c184 (patch)
treee17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/opened
parent53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff)
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r--test-suite/bugs/opened/bug_1338.v-disabled (renamed from test-suite/bugs/opened/1338.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_1596.v (renamed from test-suite/bugs/opened/1596.v)0
-rw-r--r--test-suite/bugs/opened/bug_1615.v (renamed from test-suite/bugs/opened/1615.v)1
-rw-r--r--test-suite/bugs/opened/bug_1671.v (renamed from test-suite/bugs/opened/1671.v)0
-rw-r--r--test-suite/bugs/opened/bug_1811.v (renamed from test-suite/bugs/opened/1811.v)0
-rw-r--r--test-suite/bugs/opened/bug_2572.v-disabled (renamed from test-suite/bugs/opened/2572.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3010.v-disabled (renamed from test-suite/bugs/opened/3010.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3092.v (renamed from test-suite/bugs/opened/3092.v)0
-rw-r--r--test-suite/bugs/opened/bug_3166.v (renamed from test-suite/bugs/opened/3166.v)0
-rw-r--r--test-suite/bugs/opened/bug_3186.v-disabled (renamed from test-suite/bugs/opened/3186.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3248.v (renamed from test-suite/bugs/opened/3248.v)0
-rw-r--r--test-suite/bugs/opened/bug_3277.v (renamed from test-suite/bugs/opened/3277.v)0
-rw-r--r--test-suite/bugs/opened/bug_3278.v (renamed from test-suite/bugs/opened/3278.v)0
-rw-r--r--test-suite/bugs/opened/bug_3283.v (renamed from test-suite/bugs/opened/3283.v)0
-rw-r--r--test-suite/bugs/opened/bug_3295.v (renamed from test-suite/bugs/opened/3295.v)0
-rw-r--r--test-suite/bugs/opened/bug_3304.v (renamed from test-suite/bugs/opened/3304.v)0
-rw-r--r--test-suite/bugs/opened/bug_3311.v (renamed from test-suite/bugs/opened/3311.v)0
-rw-r--r--test-suite/bugs/opened/bug_3312.v (renamed from test-suite/bugs/opened/3312.v)0
-rw-r--r--test-suite/bugs/opened/bug_3343.v (renamed from test-suite/bugs/opened/3343.v)0
-rw-r--r--test-suite/bugs/opened/bug_3345.v (renamed from test-suite/bugs/opened/3345.v)0
-rw-r--r--test-suite/bugs/opened/bug_3357.v (renamed from test-suite/bugs/opened/3357.v)0
-rw-r--r--test-suite/bugs/opened/bug_3363.v (renamed from test-suite/bugs/opened/3363.v)0
-rw-r--r--test-suite/bugs/opened/bug_3370.v (renamed from test-suite/bugs/opened/3370.v)0
-rw-r--r--test-suite/bugs/opened/bug_3395.v (renamed from test-suite/bugs/opened/3395.v)0
-rw-r--r--test-suite/bugs/opened/bug_3424.v (renamed from test-suite/bugs/opened/3424.v)0
-rw-r--r--test-suite/bugs/opened/bug_3459.v (renamed from test-suite/bugs/opened/3459.v)0
-rw-r--r--test-suite/bugs/opened/bug_3463.v (renamed from test-suite/bugs/opened/3463.v)1
-rw-r--r--test-suite/bugs/opened/bug_3478.v-disabled (renamed from test-suite/bugs/opened/3478.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3626.v (renamed from test-suite/bugs/opened/3626.v)0
-rw-r--r--test-suite/bugs/opened/bug_3655.v (renamed from test-suite/bugs/opened/3655.v)0
-rw-r--r--test-suite/bugs/opened/bug_3754.v (renamed from test-suite/bugs/opened/3754.v)0
-rw-r--r--test-suite/bugs/opened/bug_3794.v (renamed from test-suite/bugs/opened/3794.v)0
-rw-r--r--test-suite/bugs/opened/bug_3889.v (renamed from test-suite/bugs/opened/3889.v)0
-rw-r--r--test-suite/bugs/opened/bug_3890.v (renamed from test-suite/bugs/opened/3890.v)2
-rw-r--r--test-suite/bugs/opened/bug_3919.v-disabled (renamed from test-suite/bugs/opened/3919.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3922.v-disabled (renamed from test-suite/bugs/opened/3922.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3928.v-disabled (renamed from test-suite/bugs/opened/3928.v-disabled)0
-rw-r--r--test-suite/bugs/opened/bug_3938.v (renamed from test-suite/bugs/opened/3938.v)0
-rw-r--r--test-suite/bugs/opened/bug_3946.v (renamed from test-suite/bugs/opened/3946.v)0
-rw-r--r--test-suite/bugs/opened/bug_4701.v (renamed from test-suite/bugs/opened/4701.v)0
-rw-r--r--test-suite/bugs/opened/bug_4721.v (renamed from test-suite/bugs/opened/4721.v)0
-rw-r--r--test-suite/bugs/opened/bug_4728.v (renamed from test-suite/bugs/opened/4728.v)0
-rw-r--r--test-suite/bugs/opened/bug_4755.v (renamed from test-suite/bugs/opened/4755.v)0
-rw-r--r--test-suite/bugs/opened/bug_4771.v (renamed from test-suite/bugs/opened/4771.v)0
-rw-r--r--test-suite/bugs/opened/bug_4778.v (renamed from test-suite/bugs/opened/4778.v)0
-rw-r--r--test-suite/bugs/opened/bug_4781.v (renamed from test-suite/bugs/opened/4781.v)0
-rw-r--r--test-suite/bugs/opened/bug_4813.v (renamed from test-suite/bugs/opened/4813.v)0
-rw-r--r--test-suite/bugs/opened/bug_6393.v (renamed from test-suite/bugs/opened/6393.v)0
-rw-r--r--test-suite/bugs/opened/bug_6602.v (renamed from test-suite/bugs/opened/6602.v)0
49 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/1338.v-disabled b/test-suite/bugs/opened/bug_1338.v-disabled
index ab0f98202d..ab0f98202d 100644
--- a/test-suite/bugs/opened/1338.v-disabled
+++ b/test-suite/bugs/opened/bug_1338.v-disabled
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/bug_1596.v
index 820022d995..820022d995 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
diff --git a/test-suite/bugs/opened/1615.v b/test-suite/bugs/opened/bug_1615.v
index 2825701410..c045335410 100644
--- a/test-suite/bugs/opened/1615.v
+++ b/test-suite/bugs/opened/bug_1615.v
@@ -9,4 +9,3 @@ Lemma foo' : forall n m : nat, n <= n + n * m.
Proof.
intros. Fail omega.
Abort.
-
diff --git a/test-suite/bugs/opened/1671.v b/test-suite/bugs/opened/bug_1671.v
index b4e653f687..b4e653f687 100644
--- a/test-suite/bugs/opened/1671.v
+++ b/test-suite/bugs/opened/bug_1671.v
diff --git a/test-suite/bugs/opened/1811.v b/test-suite/bugs/opened/bug_1811.v
index 57c1744313..57c1744313 100644
--- a/test-suite/bugs/opened/1811.v
+++ b/test-suite/bugs/opened/bug_1811.v
diff --git a/test-suite/bugs/opened/2572.v-disabled b/test-suite/bugs/opened/bug_2572.v-disabled
index 3f6c6a0d14..3f6c6a0d14 100644
--- a/test-suite/bugs/opened/2572.v-disabled
+++ b/test-suite/bugs/opened/bug_2572.v-disabled
diff --git a/test-suite/bugs/opened/3010.v-disabled b/test-suite/bugs/opened/bug_3010.v-disabled
index f2906bd6a6..f2906bd6a6 100644
--- a/test-suite/bugs/opened/3010.v-disabled
+++ b/test-suite/bugs/opened/bug_3010.v-disabled
diff --git a/test-suite/bugs/opened/3092.v b/test-suite/bugs/opened/bug_3092.v
index 9db21d156e..9db21d156e 100644
--- a/test-suite/bugs/opened/3092.v
+++ b/test-suite/bugs/opened/bug_3092.v
diff --git a/test-suite/bugs/opened/3166.v b/test-suite/bugs/opened/bug_3166.v
index e1c29a954c..e1c29a954c 100644
--- a/test-suite/bugs/opened/3166.v
+++ b/test-suite/bugs/opened/bug_3166.v
diff --git a/test-suite/bugs/opened/3186.v-disabled b/test-suite/bugs/opened/bug_3186.v-disabled
index d0bcb920cc..d0bcb920cc 100644
--- a/test-suite/bugs/opened/3186.v-disabled
+++ b/test-suite/bugs/opened/bug_3186.v-disabled
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/bug_3248.v
index 33c408a28c..33c408a28c 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/bug_3248.v
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/bug_3277.v
index 5f4231363a..5f4231363a 100644
--- a/test-suite/bugs/opened/3277.v
+++ b/test-suite/bugs/opened/bug_3277.v
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/bug_3278.v
index 1c6deae94b..1c6deae94b 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/bug_3278.v
diff --git a/test-suite/bugs/opened/3283.v b/test-suite/bugs/opened/bug_3283.v
index 3ab5416e8c..3ab5416e8c 100644
--- a/test-suite/bugs/opened/3283.v
+++ b/test-suite/bugs/opened/bug_3283.v
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/bug_3295.v
index c09649de73..c09649de73 100644
--- a/test-suite/bugs/opened/3295.v
+++ b/test-suite/bugs/opened/bug_3295.v
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/bug_3304.v
index 66668930c7..66668930c7 100644
--- a/test-suite/bugs/opened/3304.v
+++ b/test-suite/bugs/opened/bug_3304.v
diff --git a/test-suite/bugs/opened/3311.v b/test-suite/bugs/opened/bug_3311.v
index 1c66bc1e55..1c66bc1e55 100644
--- a/test-suite/bugs/opened/3311.v
+++ b/test-suite/bugs/opened/bug_3311.v
diff --git a/test-suite/bugs/opened/3312.v b/test-suite/bugs/opened/bug_3312.v
index 749921e2f6..749921e2f6 100644
--- a/test-suite/bugs/opened/3312.v
+++ b/test-suite/bugs/opened/bug_3312.v
diff --git a/test-suite/bugs/opened/3343.v b/test-suite/bugs/opened/bug_3343.v
index 6c5a85f9cf..6c5a85f9cf 100644
--- a/test-suite/bugs/opened/3343.v
+++ b/test-suite/bugs/opened/bug_3343.v
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/bug_3345.v
index 3e3da6df71..3e3da6df71 100644
--- a/test-suite/bugs/opened/3345.v
+++ b/test-suite/bugs/opened/bug_3345.v
diff --git a/test-suite/bugs/opened/3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..c479158877 100644
--- a/test-suite/bugs/opened/3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/bug_3363.v
index 800d89573c..800d89573c 100644
--- a/test-suite/bugs/opened/3363.v
+++ b/test-suite/bugs/opened/bug_3363.v
diff --git a/test-suite/bugs/opened/3370.v b/test-suite/bugs/opened/bug_3370.v
index 4964bf96c0..4964bf96c0 100644
--- a/test-suite/bugs/opened/3370.v
+++ b/test-suite/bugs/opened/bug_3370.v
diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/bug_3395.v
index 5ca48fc9d6..5ca48fc9d6 100644
--- a/test-suite/bugs/opened/3395.v
+++ b/test-suite/bugs/opened/bug_3395.v
diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/bug_3424.v
index d1c5bb68f9..d1c5bb68f9 100644
--- a/test-suite/bugs/opened/3424.v
+++ b/test-suite/bugs/opened/bug_3424.v
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/bug_3459.v
index 762611f751..762611f751 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/bug_3459.v
diff --git a/test-suite/bugs/opened/3463.v b/test-suite/bugs/opened/bug_3463.v
index 541db37fb7..124f2bcc03 100644
--- a/test-suite/bugs/opened/3463.v
+++ b/test-suite/bugs/opened/bug_3463.v
@@ -10,4 +10,3 @@ Goal True.
test2 nat (1 + _).
test3 (1 + _) nat.
test3 (1 + _ : nat) nat.
-
diff --git a/test-suite/bugs/opened/3478.v-disabled b/test-suite/bugs/opened/bug_3478.v-disabled
index cc926b2167..cc926b2167 100644
--- a/test-suite/bugs/opened/3478.v-disabled
+++ b/test-suite/bugs/opened/bug_3478.v-disabled
diff --git a/test-suite/bugs/opened/3626.v b/test-suite/bugs/opened/bug_3626.v
index 46a6c009eb..46a6c009eb 100644
--- a/test-suite/bugs/opened/3626.v
+++ b/test-suite/bugs/opened/bug_3626.v
diff --git a/test-suite/bugs/opened/3655.v b/test-suite/bugs/opened/bug_3655.v
index 841f77febb..841f77febb 100644
--- a/test-suite/bugs/opened/3655.v
+++ b/test-suite/bugs/opened/bug_3655.v
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/bug_3754.v
index a717bbe735..a717bbe735 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/bug_3754.v
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/bug_3794.v
index e4711a38c0..e4711a38c0 100644
--- a/test-suite/bugs/opened/3794.v
+++ b/test-suite/bugs/opened/bug_3794.v
diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/bug_3889.v
index 6b287324cc..6b287324cc 100644
--- a/test-suite/bugs/opened/3889.v
+++ b/test-suite/bugs/opened/bug_3889.v
diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/bug_3890.v
index f9ac9be2c8..5c74addb62 100644
--- a/test-suite/bugs/opened/3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -3,7 +3,7 @@ Class Bar := b : Type.
Instance foo : Foo := _.
(* 1 subgoals, subgoal 1 (ID 4)
-
+
============================
Foo *)
diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/bug_3919.v-disabled
index 0d661de9c4..0d661de9c4 100644
--- a/test-suite/bugs/opened/3919.v-disabled
+++ b/test-suite/bugs/opened/bug_3919.v-disabled
diff --git a/test-suite/bugs/opened/3922.v-disabled b/test-suite/bugs/opened/bug_3922.v-disabled
index ce4f509cad..ce4f509cad 100644
--- a/test-suite/bugs/opened/3922.v-disabled
+++ b/test-suite/bugs/opened/bug_3922.v-disabled
diff --git a/test-suite/bugs/opened/3928.v-disabled b/test-suite/bugs/opened/bug_3928.v-disabled
index b470eb229b..b470eb229b 100644
--- a/test-suite/bugs/opened/3928.v-disabled
+++ b/test-suite/bugs/opened/bug_3928.v-disabled
diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/bug_3938.v
index 2d0d1930f1..2d0d1930f1 100644
--- a/test-suite/bugs/opened/3938.v
+++ b/test-suite/bugs/opened/bug_3938.v
diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/bug_3946.v
index e77bdbc652..e77bdbc652 100644
--- a/test-suite/bugs/opened/3946.v
+++ b/test-suite/bugs/opened/bug_3946.v
diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/bug_4701.v
index 9286f0f1f0..9286f0f1f0 100644
--- a/test-suite/bugs/opened/4701.v
+++ b/test-suite/bugs/opened/bug_4701.v
diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/bug_4721.v
index 1f184b3930..1f184b3930 100644
--- a/test-suite/bugs/opened/4721.v
+++ b/test-suite/bugs/opened/bug_4721.v
diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/bug_4728.v
index 230b4beb6c..230b4beb6c 100644
--- a/test-suite/bugs/opened/4728.v
+++ b/test-suite/bugs/opened/bug_4728.v
diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/bug_4755.v
index 9cc0d361ea..9cc0d361ea 100644
--- a/test-suite/bugs/opened/4755.v
+++ b/test-suite/bugs/opened/bug_4755.v
diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/bug_4771.v
index 396d74bdbf..396d74bdbf 100644
--- a/test-suite/bugs/opened/4771.v
+++ b/test-suite/bugs/opened/bug_4771.v
diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/bug_4778.v
index 633d158e96..633d158e96 100644
--- a/test-suite/bugs/opened/4778.v
+++ b/test-suite/bugs/opened/bug_4778.v
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/bug_4781.v
index 8b651ac22e..8b651ac22e 100644
--- a/test-suite/bugs/opened/4781.v
+++ b/test-suite/bugs/opened/bug_4781.v
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/bug_4813.v
index 2ac5535934..2ac5535934 100644
--- a/test-suite/bugs/opened/4813.v
+++ b/test-suite/bugs/opened/bug_4813.v
diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/bug_6393.v
index 8d5d092333..8d5d092333 100644
--- a/test-suite/bugs/opened/6393.v
+++ b/test-suite/bugs/opened/bug_6393.v
diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/bug_6602.v
index 3690adf90a..3690adf90a 100644
--- a/test-suite/bugs/opened/6602.v
+++ b/test-suite/bugs/opened/bug_6602.v