Add appropriate Fail(s) to opened bugs

The contract is that a file in bugs/opened should not raise errors if
the bug is still open.

Some of them fail for different reasons than they used to; I'm not sure
what to do about these.

41 files changed, 135 insertions, 77 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
index 9c360c9f4..f609aff5d 100644
--- a/test-suite/bugs/opened/HoTT_coq_007.v
+++ b/test-suite/bugs/opened/HoTT_coq_007.v
@@ -36,9 +36,14 @@ Module Comment1.
   Set Printing All.
   Set Printing Universes.
 
-  Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x).
-    intro. (* Illegal application (Type Error) *)
-  Abort.
+  Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type
+ "@Functor (* Top.448 Top.449 Top.450 Top.451 *)
+    (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0
+    Empty_set Cat0" while it is expected to have type
+ "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49"
+(Universe inconsistency: Cannot enforce Set = Top.295)). *)
+  Fail intro. (* Illegal application (Type Error) *)
+  Fail Abort.
 End Comment1.
 
 Module Comment2.
@@ -106,5 +111,5 @@ Module Comment3.
   Polymorphic Hint Resolve foo. (* success *)
   Polymorphic Hint Rewrite @foo. (* Success *)
   Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
-  Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
+  Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
 End Comment3.
diff --git a/test-suite/bugs/opened/HoTT_coq_014.v b/test-suite/bugs/opened/HoTT_coq_014.v
index 1fd7e251f..109653ca2 100644
--- a/test-suite/bugs/opened/HoTT_coq_014.v
+++ b/test-suite/bugs/opened/HoTT_coq_014.v
@@ -158,7 +158,28 @@ Section GraphObj.
   Defined.
 End GraphObj.
 
-
-Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
+Set Printing Universes.
+Set Printing All.
+Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf' (C D : SmallCategory) (F : SpecializedFunctor C D) :
+  Morphism (FunctorCategory TypeCat GraphIndexingCategory) (@UnderlyingGraph (SObject C) (C:SpecializedCategory (SObject C))) (UnderlyingGraph D). (* Toplevel input, characters 216-249:
+Error:
+In environment
+C : SmallCategory (* Top.594 *)
+D : SmallCategory (* Top.595 *)
+F :
+@SpecializedFunctor (* Top.25 Set Top.25 Set *) (SObject (* Top.25 *) C)
+  (SUnderlyingCategory (* Top.25 *) C) (SObject (* Top.25 *) D)
+  (SUnderlyingCategory (* Top.25 *) D)
+The term
+ "SUnderlyingCategory (* Top.25 *) C
+  :SpecializedCategory (* Top.25 Set *) (SObject (* Top.25 *) C)" has type
+ "SpecializedCategory (* Top.618 Top.619 *) (SObject (* Top.25 *) C)"
+while it is expected to have type
+ "SpecializedCategory (* Top.224 Top.225 *) (SObject (* Top.617 *) C)"
+(Universe inconsistency: Cannot enforce Set = Top.225)).
+ *)
+Fail Admitted.
+
+Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
   Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
-Admitted.
+Fail Admitted.
diff --git a/test-suite/bugs/opened/HoTT_coq_020.v b/test-suite/bugs/opened/HoTT_coq_020.v
index 6747d6af2..ff73137a7 100644
--- a/test-suite/bugs/opened/HoTT_coq_020.v
+++ b/test-suite/bugs/opened/HoTT_coq_020.v
@@ -65,9 +65,18 @@ Section Law0.
   Set Printing Universes.
   Set Printing Existential Instances.
 
-  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
-    hnf.
-    refine (@FunctorFrom0 _ _).
+  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf' : Object (@FunctorCategory Empty_set Cat0 objC C).
+  (* In environment
+objC : Type (* Top.154 *)
+C : Category (* Top.155 Top.154 *) objC
+The term "objC" has type "Type (* Top.154 *)"
+while it is expected to have type "Type (* Top.184 *)"
+(Universe inconsistency: Cannot enforce Top.154 <= Set)). *)
+  Fail Admitted.
+
+  Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
+  Fail hnf.
+  Fail refine (@FunctorFrom0 _ _).
     (* Toplevel input, characters 23-40:
 Error:
 In environment
@@ -81,3 +90,6 @@ The term
  while it is expected to have type
  "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
 *)
+  Fail admit.
+  Fail Defined.
+End Law0.
diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index 8132f51d2..2f8ec8749 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -20,9 +20,10 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
 Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
 : FunctorToType C.
-  refine (@Build_Functor _ C _ TypeCat
+  Fail refine (@Build_Functor _ C _ TypeCat
                          (fun x => F.(ObjectOf) x)
                          (fun s d m => F.(MorphismOf) _ _ m)).
+  admit.
 Defined. (* Toplevel input, characters 0-8:
 Error:
 The term
diff --git a/test-suite/bugs/opened/HoTT_coq_029.v b/test-suite/bugs/opened/HoTT_coq_029.v
index 85a2714c7..524e91d6a 100644
--- a/test-suite/bugs/opened/HoTT_coq_029.v
+++ b/test-suite/bugs/opened/HoTT_coq_029.v
@@ -140,9 +140,9 @@ Module FirstComment.
   Section MonoidalCategory.
     Variable objC : Type.
 
-    Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
+    Fail Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
 
-    Record MonoidalCategory :=
+    Fail Record MonoidalCategory :=
       {
         MonoidalUnderlyingCategory :> @Category objC;
         TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
@@ -153,8 +153,8 @@ Module FirstComment.
   End MonoidalCategory.
 
   Section EnrichedCategory.
-    Context `(M : @MonoidalCategory objM).
-    Let x : M := IdentityObject M.
+    Fail Context `(M : @MonoidalCategory objM).
+    Fail Let x : M := IdentityObject M.
     (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report.  *)
   End EnrichedCategory.
 End FirstComment.
@@ -301,7 +301,7 @@ Module SecondComment.
     Definition CommaCategoryProjection : Functor (CommaCategory S T) (ProductCategory A B).
     Admitted.
 
-    Definition CommaCategoryProjectionFunctor_ObjectOf
+    Fail Definition CommaCategoryProjectionFunctor_ObjectOf
     : @SliceCategoryOver _ LocallySmallCat (ProductCategory A B : Category _)
       :=
         existT _
diff --git a/test-suite/bugs/opened/HoTT_coq_030.v b/test-suite/bugs/opened/HoTT_coq_030.v
index c9d8fe137..934fcd5d8 100644
--- a/test-suite/bugs/opened/HoTT_coq_030.v
+++ b/test-suite/bugs/opened/HoTT_coq_030.v
@@ -235,6 +235,7 @@ Section FullyFaithful.
   Context `(C : @SpecializedCategory objC).
 
   Set Printing Universes.
-  Check InducedHomNaturalTransformation (Yoneda C).
+  Fail Check InducedHomNaturalTransformation (Yoneda C).
   (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because
 Top.851 < Top.869 <= Top.864 <= Top.865). *)
+End FullyFaithful.
diff --git a/test-suite/bugs/opened/HoTT_coq_032.v b/test-suite/bugs/opened/HoTT_coq_032.v
index 39a7103d1..e6ae8a0c4 100644
--- a/test-suite/bugs/opened/HoTT_coq_032.v
+++ b/test-suite/bugs/opened/HoTT_coq_032.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *)
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
@@ -11,7 +11,7 @@ Delimit Scope functor_scope with functor.
 
 Local Open Scope category_scope.
 
-Record SpecializedCategory (obj : Type) :=
+Fail Record SpecializedCategory (obj : Type) :=
   {
     Object :> _ := obj;
     Morphism : obj -> obj -> Type;
diff --git a/test-suite/bugs/opened/HoTT_coq_033.v b/test-suite/bugs/opened/HoTT_coq_033.v
index c4dbf74cd..e357fce32 100644
--- a/test-suite/bugs/opened/HoTT_coq_033.v
+++ b/test-suite/bugs/opened/HoTT_coq_033.v
@@ -7,6 +7,8 @@ Monomorphic Inductive JMeq' (A : Type) (x : A)
 : forall B : Type, B -> Prop :=
   JMeq'_refl : JMeq' x x.
 
+(* Note: This should fail (the [Fail] should be present in the final file, even when in bugs/closed) *)
 Fail Monomorphic Definition foo := @JMeq' _ (@JMeq').
 
-Monomorphic Definition bar := @JMeq _ (@JMeq).
+(* Note: This should not fail *)
+Fail Monomorphic Definition bar := @JMeq _ (@JMeq).
diff --git a/test-suite/bugs/opened/HoTT_coq_034.v b/test-suite/bugs/opened/HoTT_coq_034.v
index 9697928ff..3c2b7a7d6 100644
--- a/test-suite/bugs/opened/HoTT_coq_034.v
+++ b/test-suite/bugs/opened/HoTT_coq_034.v
@@ -14,7 +14,7 @@ Module Short.
 
   Set Printing Universes.
   Check bar nat Set : Set. (* success *)
-  Check foo nat Set : Set. (* Toplevel input, characters 6-17:
+  Fail Check foo nat Set : Set. (* Toplevel input, characters 6-17:
 Error:
 The term "foo (* Top.303 Top.304 *) nat Set" has type
 "Type (* Top.304 *)" while it is expected to have type
@@ -97,8 +97,8 @@ SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
     Let TypeCatC := FunctorCategory C TypeCat.
     Let YC := (Yoneda C).
     Set Printing Universes.
-    Check @FunctorProduct' C TypeCatC (Yoneda C).
-    (* Toplevel input, characters 35-43:
+    Fail Check @FunctorProduct' C TypeCatC (Yoneda C).
+  (* Toplevel input, characters 35-43:
 Error:
 In environment
 objC : Type (* Top.186 *)
@@ -123,5 +123,6 @@ while it is expected to have type
  "Functor (* Top.216 Top.219 Top.217 Top.220 *) C TypeCatC"
 (Universe inconsistency: Cannot enforce Top.230 = Top.217 because Top.217
 <= Top.227 < Top.225 <= Top.231 <= Top.230)).
-     *)
+   *)
+  End FullyFaithful.
 End Long.
diff --git a/test-suite/bugs/opened/HoTT_coq_036.v b/test-suite/bugs/opened/HoTT_coq_036.v
index b06830dd0..3c480eea5 100644
--- a/test-suite/bugs/opened/HoTT_coq_036.v
+++ b/test-suite/bugs/opened/HoTT_coq_036.v
@@ -27,7 +27,10 @@ Module Version1.
 
   Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
     assert (Hf : focus ((S tt) = (S tt))) by constructor.
-    progress change CObject with (fun C => @Object (CObject C) C) in *.
+    let C1 := constr:(CObject) in
+    let C2 := constr:(fun C => @Object (CObject C) C) in
+    unify C1 C2.
+    Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
     simpl in *.
     match type of Hf with
       | focus ?V => exact V
@@ -74,7 +77,7 @@ Module Version2.
                                (objD : Type) (D : SpecializedCategory objD), Prop.
   Definition CommaCategory_Object (A : Category) : Type.
     assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    progress change CObject with (fun C => @Object (CObject C) C) in *;
+    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
       simpl in *.
     match type of Hf with
       | focus ?V => exact V
@@ -111,7 +114,7 @@ Module OtherBug.
                                (objD : Type) (D : SpecializedCategory objD), Prop.
   Definition CommaCategory_Object (A : Category) : Type.
     assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    progress change CObject with (fun C => @Object (CObject C) C) in *;
+    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
       simpl in *.
     match type of Hf with
       | focus ?V => exact V
diff --git a/test-suite/bugs/opened/HoTT_coq_045.v b/test-suite/bugs/opened/HoTT_coq_045.v
index 590bdd157..27b28e593 100644
--- a/test-suite/bugs/opened/HoTT_coq_045.v
+++ b/test-suite/bugs/opened/HoTT_coq_045.v
@@ -26,7 +26,10 @@ Definition focus A (_ : A) := True.
 
 Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
   assert (Hf : focus ((S tt) = (S tt))) by constructor.
-  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  let C1 := constr:(CObject) in
+  let C2 := constr:(fun C => @Object (CObject C) C) in
+  unify C1 C2.
+  Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
   simpl in *.
   let V := match type of Hf with
              | focus ?V => constr:(V)
diff --git a/test-suite/bugs/opened/HoTT_coq_052.v b/test-suite/bugs/opened/HoTT_coq_052.v
index dac575b54..886dbad9e 100644
--- a/test-suite/bugs/opened/HoTT_coq_052.v
+++ b/test-suite/bugs/opened/HoTT_coq_052.v
@@ -7,13 +7,16 @@ Goal Prop.
 Abort.
 
 Goal Prop = Set.
-  Fail match goal with |- ?x = ?x => idtac end.
+  (* This should fail *)
+  Fail Fail match goal with |- ?x = ?x => idtac end.
 Abort.
 
 Goal Type = Prop.
-  Fail match goal with |- ?x = ?x => idtac end.
+  (* This should fail *)
+  Fail Fail match goal with |- ?x = ?x => idtac end.
 Abort.
 
 Goal Type = Set.
-  Fail match goal with |- ?x = ?x => idtac end.
+  (* This should fail *)
+  Fail Fail match goal with |- ?x = ?x => idtac end.
 Abort.
diff --git a/test-suite/bugs/opened/HoTT_coq_053.v b/test-suite/bugs/opened/HoTT_coq_053.v
index a14fb6aa5..f47f9b525 100644
--- a/test-suite/bugs/opened/HoTT_coq_053.v
+++ b/test-suite/bugs/opened/HoTT_coq_053.v
@@ -29,7 +29,7 @@ Definition IndiscreteCategory X : PreCategory
   := @Build_PreCategory X
                          (fun _ _ => Unit).
 
-Definition NatCategory (n : nat) :=
+Fail Definition NatCategory (n : nat) :=
   match n with
     | 0 => IndiscreteCategory Unit
     | _ => DiscreteCategory Bool
@@ -43,7 +43,7 @@ Definition NatCategory' (n : nat) :=
     | _ => DiscreteCategory Bool
   end.
 
-Definition NatCategory'' (n : nat) :=
+Fail Definition NatCategory'' (n : nat) :=
   match n with
     | 0 => IndiscreteCategory Unit
     | _ => DiscreteCategory Bool
diff --git a/test-suite/bugs/opened/HoTT_coq_054.v b/test-suite/bugs/opened/HoTT_coq_054.v
index f79fe1c1e..fd37eb330 100644
--- a/test-suite/bugs/opened/HoTT_coq_054.v
+++ b/test-suite/bugs/opened/HoTT_coq_054.v
@@ -24,7 +24,7 @@ Defined.
 Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
   := match p with idpath => idpath end.
 
-Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
+Fail Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
               (* Fortunately, this unifies properly *)
               (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
   let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
@@ -57,8 +57,8 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inr y' => ap h
                        end
        end) pq).
-  destruct x; destruct y; destruct pq; reflexivity.
-Qed.
+  Fail destruct x; destruct y; destruct pq; reflexivity.
+Fail Qed.
 (* Toplevel input, characters 1367-1374:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/HoTT_coq_061.v b/test-suite/bugs/opened/HoTT_coq_061.v
index d1ea16ec3..7b48e4e01 100644
--- a/test-suite/bugs/opened/HoTT_coq_061.v
+++ b/test-suite/bugs/opened/HoTT_coq_061.v
@@ -116,7 +116,7 @@ Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
 Variable C : PreCategory.
 Variable D : PreCategory.
 Variable E : PreCategory.
-Definition NTWhiskerR_Functorial (G : [C, D]%category)
+Fail Definition NTWhiskerR_Functorial (G : [C, D]%category)
 : [[D, E], [C, E]]%category
   := Build_Functor
        [C, D] [C, E]
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index 6c0221479..99c2a1fb5 100644
--- a/test-suite/bugs/opened/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
@@ -70,8 +70,8 @@ Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
   intro f.
   Set Printing Universes.
   Set Printing All.
-  pose proof (apD f (path_universe e)).
-  pose proof (apD f p).
+  Fail pose proof (apD f (path_universe e)).
+  Fail pose proof (apD f p).
 (* Toplevel input, characters 18-19:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/HoTT_coq_063.v b/test-suite/bugs/opened/HoTT_coq_063.v
index 1c584d295..8656fadaa 100644
--- a/test-suite/bugs/opened/HoTT_coq_063.v
+++ b/test-suite/bugs/opened/HoTT_coq_063.v
@@ -8,7 +8,7 @@ Module A.
   | BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
   | trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
 
-  Existing Class IsTrunc.
+  Fail Existing Class IsTrunc.
   (* Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
 End A.
@@ -20,7 +20,7 @@ Module B.
       | S _ => False
     end.
 
-  Existing Class IsTrunc.
+  Fail Existing Class IsTrunc.
   (* Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
 End B.
diff --git a/test-suite/bugs/opened/HoTT_coq_064.v b/test-suite/bugs/opened/HoTT_coq_064.v
index fae954f81..98e815aef 100644
--- a/test-suite/bugs/opened/HoTT_coq_064.v
+++ b/test-suite/bugs/opened/HoTT_coq_064.v
@@ -180,7 +180,7 @@ Section bar.
 
   Variable D : PreCategory.
 
-  Context `(has_colimits
+  Fail Context `(has_colimits
             : forall F : Functor D C,
                 @IsColimit _ C D F (colimits F)).
 (* Error: Unsatisfied constraints: Top.3773 <= Set
diff --git a/test-suite/bugs/opened/HoTT_coq_078.v b/test-suite/bugs/opened/HoTT_coq_078.v
index 6c02cad56..a2c97d067 100644
--- a/test-suite/bugs/opened/HoTT_coq_078.v
+++ b/test-suite/bugs/opened/HoTT_coq_078.v
@@ -35,7 +35,7 @@ Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
        | idpath => idpath
      end. (* success *)
 
-Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
+Fail Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
   (z : P a * Q a)
   : transport (fun a => P a * Q a) p z  =  (transport _ p (fst z), transport _ p (snd z))
   := match p with
diff --git a/test-suite/bugs/opened/HoTT_coq_080.v b/test-suite/bugs/opened/HoTT_coq_080.v
index 36f478002..9f6949d39 100644
--- a/test-suite/bugs/opened/HoTT_coq_080.v
+++ b/test-suite/bugs/opened/HoTT_coq_080.v
@@ -23,7 +23,7 @@ Definition sum_category (C D : category) : category :=
 Goal forall C D (x y : ob (sum_category C D)), Type.
 intros C D x y.
 hnf in x, y.
-exact (hom x y). (* Toplevel input, characters 26-27:
+Fail exact (hom x y). (* Toplevel input, characters 26-27:
 Error:
 In environment
 C : category
diff --git a/test-suite/bugs/opened/HoTT_coq_081.v b/test-suite/bugs/opened/HoTT_coq_081.v
index 6de3ebdbd..bcd12aa69 100644
--- a/test-suite/bugs/opened/HoTT_coq_081.v
+++ b/test-suite/bugs/opened/HoTT_coq_081.v
@@ -7,6 +7,6 @@ Record category :=
     hom : ob -> ob -> Type
   }.
 
-Record foo := { C : category; x :> ob C }.
+Fail Record foo := { C : category; x :> ob C }.
 (* Toplevel input, characters 0-42:
 Error: Cannot find the target class. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_082.v b/test-suite/bugs/opened/HoTT_coq_082.v
index 03886695c..257afe0b6 100644
--- a/test-suite/bugs/opened/HoTT_coq_082.v
+++ b/test-suite/bugs/opened/HoTT_coq_082.v
@@ -4,16 +4,16 @@ Set Universe Polymorphism.
 Record category :=
   { ob : Type }.
 
-Existing Class category. (*
+Fail Existing Class category. (*
 Toplevel input, characters 0-24:
 Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
 
 Record category' :=
-  { ob : Type;
-    hom : ob -> ob -> Type }.
+  { ob' : Type;
+    hom' : ob' -> ob' -> Type }.
 
-Existing Class category'. (*
+Fail Existing Class category'. (*
 Toplevel input, characters 0-24:
 Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
index 494b25c7b..091720272 100644
--- a/test-suite/bugs/opened/HoTT_coq_083.v
+++ b/test-suite/bugs/opened/HoTT_coq_083.v
@@ -24,6 +24,6 @@ generalize dependent (@ob C).
   ============================
    Type -> ob C
 (dependent evars:) *)
-intros T t.
+Fail intros T t.
 (* Toplevel input, characters 9-10:
 Error: No product even after head-reduction. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_084.v b/test-suite/bugs/opened/HoTT_coq_084.v
index d007e4e23..5568ec244 100644
--- a/test-suite/bugs/opened/HoTT_coq_084.v
+++ b/test-suite/bugs/opened/HoTT_coq_084.v
@@ -37,7 +37,7 @@ Module failure.
     Variable g : group.
     Variable comp : carrier g -> carrier g -> carrier g.
 
-    Check comp 1 1.
+    Fail Check comp 1 1.
     (* Toplevel input, characters 11-12:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/HoTT_coq_085.v b/test-suite/bugs/opened/HoTT_coq_085.v
index 041c67997..43ca6864f 100644
--- a/test-suite/bugs/opened/HoTT_coq_085.v
+++ b/test-suite/bugs/opened/HoTT_coq_085.v
@@ -67,7 +67,7 @@ Module failure.
   Check ((_ o _) _2 _)%hom. (* ((?14 o ?15)%functor _1 ?18)%hom
      : hom ?13 (ob_of (?14 o ?15)%functor ?16)
          (ob_of (?14 o ?15)%functor ?17) *)
-  Check ((_ o _) _1 _)%hom. (* Toplevel input, characters 7-19:
+  Fail Check ((_ o _) _1 _)%hom. (* Toplevel input, characters 7-19:
 Error:
 The term "(?23 o ?24)%hom" has type "hom ?19 ?20 ?22"
 while it is expected to have type "functor ?25 ?26". *)
diff --git a/test-suite/bugs/opened/HoTT_coq_089.v b/test-suite/bugs/opened/HoTT_coq_089.v
index 54ae4704a..143f60404 100644
--- a/test-suite/bugs/opened/HoTT_coq_089.v
+++ b/test-suite/bugs/opened/HoTT_coq_089.v
@@ -11,7 +11,7 @@ Check comp_type_paths.
 
 Inductive type_paths' (A : Type) : Type -> Prop
   := idtypepath' : type_paths' A A
-   | other_type_path : False -> forall B : Set, type_paths' A B.
+   | other_type_path : False -> forall B : Type, type_paths' A B.
 Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
 Check comp_type_paths'.
 (* comp_type_paths'
@@ -29,7 +29,7 @@ Defined.
 
 Goal Type.
 Proof.
-  match type of comp_type_paths with
+  Fail match type of comp_type_paths with
     | ?U0 -> ?U1 -> ?R
       => exact (@comp_type_paths nat U0)
   end.
@@ -39,4 +39,5 @@ The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
 while it is expected to have type "Type (* Top.51 *)"
 (Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
 = Top.51)). *)
+  admit.
 Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_098.v b/test-suite/bugs/opened/HoTT_coq_098.v
index 1e7be20d5..a07f2f0fa 100644
--- a/test-suite/bugs/opened/HoTT_coq_098.v
+++ b/test-suite/bugs/opened/HoTT_coq_098.v
@@ -62,8 +62,8 @@ End failure.
 
 Module polycontext.
   Section SpecializedFunctor.
-    Polymorphic Context `(C : @SpecializedCategory objC).
-    Polymorphic Context `(D : @SpecializedCategory objD).
+    Context `(C : @SpecializedCategory objC).
+    Context `(D : @SpecializedCategory objD).
 
     Polymorphic Record SpecializedFunctor
       := {
diff --git a/test-suite/bugs/opened/HoTT_coq_101.v b/test-suite/bugs/opened/HoTT_coq_101.v
index 9c89a6ab9..9419c25c3 100644
--- a/test-suite/bugs/opened/HoTT_coq_101.v
+++ b/test-suite/bugs/opened/HoTT_coq_101.v
@@ -72,6 +72,6 @@ Section FullyFaithful.
   Let TypeCatC := FunctorCategory C TypeCat.
   Let YC := (Yoneda C).
   Set Printing Universes.
-  Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
+  Fail Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
 Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because
 Top.186 <= Top.189 < Top.191 <= Top.187). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_102.v b/test-suite/bugs/opened/HoTT_coq_102.v
index 72b4ffe94..9d87517e1 100644
--- a/test-suite/bugs/opened/HoTT_coq_102.v
+++ b/test-suite/bugs/opened/HoTT_coq_102.v
@@ -19,5 +19,9 @@ Definition focus A (_ : A) := True.
 
 Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
   assert (Hf : focus ((S tt) = (S tt))) by constructor.
-  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  let C1 := constr:(CObject) in
+  let C2 := constr:(fun C => @Object (CObject C) C) in
+  let check := constr:(eq_refl : C1 = C2) in
+  unify C1 C2.
+  Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
   (* not convertible *)
diff --git a/test-suite/bugs/opened/HoTT_coq_103.v b/test-suite/bugs/opened/HoTT_coq_103.v
index 7b1dc8dea..7ecf7671e 100644
--- a/test-suite/bugs/opened/HoTT_coq_103.v
+++ b/test-suite/bugs/opened/HoTT_coq_103.v
@@ -1,4 +1,4 @@
-Check (nat : Type) : Set.
+Fail Check (nat : Type) : Set.
 (* Error:
 The term "nat:Type" has type "Type" while it is expected to have type
 "Set" (Universe inconsistency). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_104.v b/test-suite/bugs/opened/HoTT_coq_104.v
index 5bb7fa8c1..ff2da3948 100644
--- a/test-suite/bugs/opened/HoTT_coq_104.v
+++ b/test-suite/bugs/opened/HoTT_coq_104.v
@@ -10,4 +10,4 @@ Local Set Primitive Projections.
 Record prod (A B : Type) : Type :=
   pair { fst : A; snd : B }.
 
-Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
+Fail Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
diff --git a/test-suite/bugs/opened/HoTT_coq_105.v b/test-suite/bugs/opened/HoTT_coq_105.v
index 86001d26e..dcef0e886 100644
--- a/test-suite/bugs/opened/HoTT_coq_105.v
+++ b/test-suite/bugs/opened/HoTT_coq_105.v
@@ -11,7 +11,7 @@ Record category :=
     hom : ob -> ob -> Type
   }.
 Set Printing All.
-Definition sum_category (C D : category) : category :=
+Fail Definition sum_category (C D : category) : category :=
   {|
     ob := sum (ob C) (ob D);
     hom x y := match x, y with
diff --git a/test-suite/bugs/opened/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v
index d3ef9f58c..8d36abc0e 100644
--- a/test-suite/bugs/opened/HoTT_coq_106.v
+++ b/test-suite/bugs/opened/HoTT_coq_106.v
@@ -8,7 +8,7 @@ Instance ispointed_forall `{H : forall a : A, IsPointed (B a)}
 : IsPointed (forall a, B a)
   := fun a => @point (B a) (H a).
 
-Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
+Fail Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
 : IsPointed (sigT B).
 (* Toplevel input, characters 20-108:
 Error: Unable to satisfy the following constraints:
diff --git a/test-suite/bugs/opened/HoTT_coq_107.v b/test-suite/bugs/opened/HoTT_coq_107.v
index c3a83627e..f8b595d85 100644
--- a/test-suite/bugs/opened/HoTT_coq_107.v
+++ b/test-suite/bugs/opened/HoTT_coq_107.v
@@ -70,7 +70,7 @@ Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B}
 Proof.
   Set Printing All.
   Set Printing Universes.
-  refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
+  Fail refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
   (* Toplevel input, characters 23-76:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/HoTT_coq_110.v b/test-suite/bugs/opened/HoTT_coq_110.v
index 5ec40dbcb..c9874f898 100644
--- a/test-suite/bugs/opened/HoTT_coq_110.v
+++ b/test-suite/bugs/opened/HoTT_coq_110.v
@@ -19,5 +19,5 @@ Module Y.
   Definition foo : (A = B) * (A = B).
     split; abstract (rewrite <- P; reflexivity).
   (* Error: internal_paths_rew already exists. *)
-  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-End Y.
+  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+Fail End Y.
diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v
index 56feadb40..825a26e16 100644
--- a/test-suite/bugs/opened/HoTT_coq_111.v
+++ b/test-suite/bugs/opened/HoTT_coq_111.v
@@ -6,9 +6,10 @@ Module X.
   Axioms A B : Type.
   Axiom P : A = B.
   Definition foo : A = B.
-    abstract (rewrite <- P; reflexivity).
+    Fail abstract (rewrite <- P; reflexivity).
   (* Error: internal_paths_rew already exists. *)
-  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+  Admitted.
+  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
 End X.
 
 Module Y.
@@ -19,7 +20,7 @@ Module Y.
   Axioms A B : Type.
   Axiom P : A = B.
   Definition foo : (A = B) * (A = B).
-    split; abstract (rewrite <- P; reflexivity).
+    Fail split; abstract (rewrite <- P; reflexivity).
   (* Error: internal_paths_rew already exists. *)
-  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-End Y.
+  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+Fail End Y.
diff --git a/test-suite/bugs/opened/HoTT_coq_113.v b/test-suite/bugs/opened/HoTT_coq_113.v
index 3ef531bc9..ae489e5f5 100644
--- a/test-suite/bugs/opened/HoTT_coq_113.v
+++ b/test-suite/bugs/opened/HoTT_coq_113.v
@@ -12,7 +12,7 @@ Proof.
   admit.
 Defined.
 Definition foo := @Bar nat.
-Check @foo Set.
+Fail Check @foo Set.
 (* Toplevel input, characters 26-29:
 Error:
 The term "Set" has type "Type (* Set+1 *)" while it is expected to have type
diff --git a/test-suite/bugs/opened/HoTT_coq_115.v b/test-suite/bugs/opened/HoTT_coq_115.v
index c1e133eeb..0a7cca31a 100644
--- a/test-suite/bugs/opened/HoTT_coq_115.v
+++ b/test-suite/bugs/opened/HoTT_coq_115.v
@@ -1 +1 @@
-Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *)
+Fail Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7a0494911..7847c5e44 100644
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ b/test-suite/bugs/opened/HoTT_coq_120.v
@@ -118,14 +118,14 @@ Section fully_faithful_helpers.
   Let isequiv_isepi_ismono_helper ua := (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).
 
   Goal True.
-  set (isequiv_isepimorphism_ismonomorphism
+  Fail set (isequiv_isepimorphism_ismonomorphism
        := fun `{Univalence}
               (Hepi : IsEpimorphism (m : morphism set_cat x y))
               (Hmono : IsMonomorphism (m : morphism set_cat x y))
           => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
   admit.
   Undo.
-  set (isequiv_isepimorphism_ismonomorphism'
+  Fail set (isequiv_isepimorphism_ismonomorphism'
        := fun `{Univalence}
               (Hepi : IsEpimorphism (m : morphism set_cat x y))
               (Hmono : IsMonomorphism (m : morphism set_cat x y))
diff --git a/test-suite/bugs/opened/HoTT_coq_122.v b/test-suite/bugs/opened/HoTT_coq_122.v
index 1ba8e5c34..7e474d0a1 100644
--- a/test-suite/bugs/opened/HoTT_coq_122.v
+++ b/test-suite/bugs/opened/HoTT_coq_122.v
@@ -22,4 +22,4 @@ Record PreCategory :=
       left_identity : forall a b (f : morphism a b), identity b o f = f
     }.
 
-Hint Rewrite @left_identity. (* stack overflow *)
+Fail Timeout 1 Hint Rewrite @left_identity. (* stack overflow *)
diff --git a/test-suite/bugs/opened/HoTT_coq_124.v b/test-suite/bugs/opened/HoTT_coq_124.v
index e6e90ada8..2854c3ee4 100644
--- a/test-suite/bugs/opened/HoTT_coq_124.v
+++ b/test-suite/bugs/opened/HoTT_coq_124.v
@@ -9,7 +9,7 @@ Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }.
 
 Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *)
 Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *)
-Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
+Fail Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
 The term
  "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
 has type
@@ -18,7 +18,7 @@ has type
 while it is expected to have type
  "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})
     (fun x : prodp Set Set => x)". *)
-Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
+Fail Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
 The term
  "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
 has type