9 files changed, 11 insertions, 12 deletions
diff --git a/test-suite/bugs/opened/2310.v b/test-suite/bugs/closed/2310.v
index a635e6083e..0be859eddf 100644
--- a/test-suite/bugs/opened/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,4 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. Fail refine (Cons (cast H _ y)).
-\ No newline at end of file
+intros. refine (Cons (cast H _ y)).
+\ No newline at end of file
diff --git a/test-suite/bugs/opened/3337.v b/test-suite/bugs/closed/3337.v
index 06acd020a9..cd7891f112 100644
--- a/test-suite/bugs/opened/3337.v
+++ b/test-suite/bugs/closed/3337.v
@@ -1,4 +1,4 @@
 Require Import Setoid.
 Goal forall x y : Set, x = y -> x = y.
 intros x y H.
-Fail rewrite_strat subterms H.
+rewrite_strat subterms H.
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index ebc79e4f9b..43108ab4b9 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -13,7 +13,7 @@ Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
 Check (fun r : @rimpl true 0 => @foo true 0 r 0).
 Check (fun r : @rimpl true 0 => foo r (x:=0)).
 Check (fun r : @rimpl true 0 => @foo _ _ r 0).
-Check (fun r : @rimpl true 0 => r.(@foo _ _)).
+Check (fun r : @rimpl true 0 => r.(@foo)).
 Check (fun r : @rimpl true 0 => r.(foo)).
 
 Notation "{ x : T  & P }" := (@sigT T P).
diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
index 1f180cd94b..89d476dcb1 100644
--- a/test-suite/bugs/closed/3481.v
+++ b/test-suite/bugs/closed/3481.v
@@ -37,7 +37,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B)
 Definition conv : @prod_rect = @prod_rect'.
 Proof. reflexivity. Defined.
 
-Fail Definition imposs :=
+Definition imposs :=
   (fun A B P f (p : prod A B) => match p as p0 return P p0 with
                                    | {| fst := x ; snd := x0 |} => f x x0
                                  end).
diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v
index 34a5e73da7..cf3f9dbefa 100644
--- a/test-suite/bugs/closed/3482.v
+++ b/test-suite/bugs/closed/3482.v
@@ -1,6 +1,6 @@
 Set Primitive Projections.
 Class Foo (F : False) := { foo : True }.
-Arguments foo F {Foo}.
+Arguments foo F {f}.
 Print Implicit foo. (* foo : forall F : False, Foo F -> True
 
 Argument Foo is implicit and maximally inserted *)
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index a193f3888a..66d653c52d 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 8657 lines to
 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines,
 then from 51 lines to 37 lines, then from 43 lines to 30 lines *)
@@ -19,7 +18,7 @@ Open Scope type_scope.
 
 Definition iff A B := prod (A -> B) (B -> A).
 Infix "<->" := iff : type_scope.
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x =
+Inductive paths {A : Type@{i}} (a : A) : A -> Type@{i} := idpath : paths a a where "x =
 y" := (@paths _ x y) : type_scope.
 Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center
 = y) }.
diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v
index 38a0a7b921..679721667a 100644
--- a/test-suite/bugs/closed/3563.v
+++ b/test-suite/bugs/closed/3563.v
@@ -16,8 +16,8 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0)
        transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7.
   intros.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2))))] ]
-      => let bar := context ctx [g] in set(foo:=h); idtac
+    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
+      => set(foo:=h); idtac
   end.
   match goal with
     | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ]
diff --git a/test-suite/bugs/closed/HoTT_coq_013.v b/test-suite/bugs/closed/HoTT_coq_013.v
index cc5ed86266..13962d5b96 100644
--- a/test-suite/bugs/closed/HoTT_coq_013.v
+++ b/test-suite/bugs/closed/HoTT_coq_013.v
@@ -1,9 +1,9 @@
 Set Implicit Arguments.
 Generalizable All Variables.
 
-Polymorphic Record Category (obj : Type) :=.
+Polymorphic Variant Category (obj : Type) :=.
 
-            Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=.
+            Polymorphic Variant Functor objC (C : Category objC) objD (D : Category objD) :=.
 
             Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
 Admitted.
diff --git a/test-suite/bugs/opened/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index 68d3056619..db3b60edae 100644
--- a/test-suite/bugs/opened/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -36,4 +36,4 @@ Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
 Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
 
 (* Check for the recursion principle I want *)
-Fail Check eq_refl : @prod_rect = @prod_rect'.
+Check eq_refl : @prod_rect = @prod_rect'.