Mark some progress in the HoTT/coq test-suite

I've marked new failing commands that I'm confused about with "???"; I'm
not sure whether or not they should fail there, but we should keep the
test-suite compiling, probably.

5 files changed, 59 insertions, 17 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
index 63e3220c55..f609aff5d7 100644
--- a/test-suite/bugs/opened/HoTT_coq_007.v
+++ b/test-suite/bugs/opened/HoTT_coq_007.v
@@ -36,14 +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). (** ??? The term "y" has type
+  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)). *)
-    intro. (* Illegal application (Type Error) *)
-  Abort.
+  Fail intro. (* Illegal application (Type Error) *)
+  Fail Abort.
 End Comment1.
 
 Module Comment2.
diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index 3a8a2cf0c4..e58092eb6f 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -18,11 +18,29 @@ Definition FunctorToType `(C : @Category objC) := Functor C TypeCat.
 (* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *)
 Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
+Set Printing Universes.
 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)).
+(* ??? Toplevel input, characters 8-148:
+Error:
+In environment
+objC : Type{Top.100}
+C : Category@{Top.100 Top.101} objC
+F : FunctorToSet@{Top.100 Top.101 Top.99} C
+The term
+ "{|
+  ObjectOf := fun x : objC => F x;
+  MorphismOf := fun (s d : objC) (m : Morphism@{Top.100 Top.101} C s d) =>
+                MorphismOf@{Top.100 Top.101 Top.99 Set} F s d m |}" has type
+ "Functor@{Top.104 Top.105 Top.106 Top.107} C TypeCat@{Top.108 Top.109
+    Top.110}" while it is expected to have type
+ "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C"
+(Universe inconsistency: Cannot enforce Set = Top.103)).
+ *)
+admit.
 Defined. (* Toplevel input, characters 0-8:
 Error:
 The term
@@ -49,12 +67,12 @@ Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) :=
 Section SetGrothendieckCoercion.
   Context `(C : @Category objC).
   Variable F : Functor C SetCat.
-  Fail Let F' := (F : FunctorToSet _) : FunctorToType _. (* The command has indeed failed with message:
+  Let F' := (F : FunctorToSet _) : FunctorToType _. (* The command has indeed failed with message:
 => Anomaly: apply_coercion_args: mismatch between arguments and coercion.
 Please report. *)
 
   Set Printing Universes.
-  Fail Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
+  Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
     := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}.
   (* Toplevel input, characters 0-187:
 Error: Illegal application:
diff --git a/test-suite/bugs/opened/HoTT_coq_029.v b/test-suite/bugs/opened/HoTT_coq_029.v
index 524e91d6ae..57f3fd22cf 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.
 
-    Fail Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
+    Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
 
-    Fail Record MonoidalCategory :=
+    Record MonoidalCategory :=
       {
         MonoidalUnderlyingCategory :> @Category objC;
         TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
@@ -153,8 +153,8 @@ Module FirstComment.
   End MonoidalCategory.
 
   Section EnrichedCategory.
-    Fail Context `(M : @MonoidalCategory objM).
-    Fail Let x : M := IdentityObject M.
+    Context `(M : @MonoidalCategory objM).
+    Let x : M := IdentityObject M.
     (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report.  *)
   End EnrichedCategory.
 End FirstComment.
@@ -311,5 +311,20 @@ Module SecondComment.
                                 (SliceCategory_Functor LocallySmallCat
                                                        (ProductCategory A B : Category _)).
     (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
+    (* Toplevel input, characters 110-142:
+Error:
+In environment
+objA : Type
+A : Category objA
+objB : Type
+B : Category objB
+objC : Type
+C : Category objC
+S : OppositeCategory (FunctorCategory A C)
+T : FunctorCategory B C
+The term "ProductCategory A B:Category (objA * objB)" has type
+ "Category (objA * objB)" while it is expected to have type
+ "Object LocallySmallCat".
+ *)
   End CommaCategoryProjectionFunctor.
 End SecondComment.
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index ce35818efd..35d23efe98 100644
--- a/test-suite/bugs/opened/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
@@ -70,7 +70,15 @@ 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)).
+  Fail pose proof (apD f (path_universe e)).
+  (* ??? Toplevel input, characters 0-37:
+Error:
+Unable to satisfy the following constraints:
+In environment:
+H : Univalence@{Top.144 Top.145 Top.146 Top.147 Top.148}
+f : forall (A : Type{Top.150}) (_ : forall _ : forall _ : A, False, False), A
+
+?57 : "@IsEquiv@{Top.150 Top.145} Bool Bool (equiv_fun@{Set Set} Bool Bool e)" *)
   Fail pose proof (apD f p).
 (* Toplevel input, characters 18-19:
 Error:
diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v
index 825a26e167..deb8e61235 100644
--- a/test-suite/bugs/opened/HoTT_coq_111.v
+++ b/test-suite/bugs/opened/HoTT_coq_111.v
@@ -6,10 +6,10 @@ Module X.
   Axioms A B : Type.
   Axiom P : A = B.
   Definition foo : A = B.
-    Fail abstract (rewrite <- P; reflexivity).
-  (* Error: internal_paths_rew already exists. *)
+    abstract (rewrite <- P; reflexivity).
+    (* Error: internal_paths_rew already exists. *)
+  Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
   Admitted.
-  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
 End X.
 
 Module Y.
@@ -20,7 +20,8 @@ Module Y.
   Axioms A B : Type.
   Axiom P : A = B.
   Definition foo : (A = B) * (A = B).
-    Fail split; abstract (rewrite <- P; reflexivity).
+    split; abstract (rewrite <- P; reflexivity).
   (* Error: internal_paths_rew already exists. *)
-  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-Fail End Y.
+  Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+  Admitted.
+End Y.