Merge branch 'v8.5'

10 files changed, 9 insertions, 1 deletions

diff --git a/test-suite/bugs/opened/2951.v b/test-suite/bugs/opened/2951.v
deleted file mode 100644
index 3739247b6b..0000000000
--- a/test-suite/bugs/opened/2951.v
+++ /dev/null
@@ -1 +0,0 @@
-Class C (A: Type) : Type := { f: A }.
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
index 6de13f74e3..f0c707bd10 100644
--- a/test-suite/bugs/opened/3263.v
+++ b/test-suite/bugs/opened/3263.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
 Generalizable All Variables.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v
index b61174a865..3e3da6df71 100644
--- a/test-suite/bugs/opened/3345.v
+++ b/test-suite/bugs/opened/3345.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *)
 Global Set Implicit Arguments.
 Require Import Coq.Lists.List Program.
diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v
index ff0dbf9745..5ca48fc9d6 100644
--- a/test-suite/bugs/opened/3395.v
+++ b/test-suite/bugs/opened/3395.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
 Generalizable All Variables.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
index 02e47a8b48..3913bbb43f 100644
--- a/test-suite/bugs/opened/3509.v
+++ b/test-suite/bugs/opened/3509.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Lemma match_bool_fn b A B xT xF
 : match b as b return forall x : A, B b x with
     | true => xT
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
index 25285636b3..daf265071a 100644
--- a/test-suite/bugs/opened/3510.v
+++ b/test-suite/bugs/opened/3510.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Lemma match_option_fn T (b : option T) A B s n
 : match b as b return forall x : A, B b x with
     | Some k => s k
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
index d647b5a83d..b2b5db6be7 100644
--- a/test-suite/bugs/opened/3685.v
+++ b/test-suite/bugs/opened/3685.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Class Funext := { }.
 Delimit Scope category_scope with category.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index c744188201..9b3f94d917 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
    coqtop version trunk (October 2014) *)
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
index 9413daa041..a03e8ffdab 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/opened/3848.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
 Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
 Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7847c5e441..05ee6c7b60 100644
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ b/test-suite/bugs/opened/HoTT_coq_120.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
 Set Universe Polymorphism.
 Generalizable All Variables.