Update various polyproj bugs w.r.t. latest trunk

12 files changed, 31 insertions, 23 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index 3c480eea5f..f10856bc7e 100644
--- a/test-suite/bugs/opened/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -30,7 +30,7 @@ Module Version1.
     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 *.
+    progress change CObject with (fun C => @Object (CObject C) C) in *.
     simpl in *.
     match type of Hf with
       | focus ?V => exact V
@@ -77,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.
-    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
+    progress change CObject with (fun C => @Object (CObject C) C) in *;
       simpl in *.
     match type of Hf with
       | focus ?V => exact V
@@ -114,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.
-    Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
+    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/closed/HoTT_coq_045.v
index 27b28e593f..00588ffb0f 100644
--- a/test-suite/bugs/opened/HoTT_coq_045.v
+++ b/test-suite/bugs/closed/HoTT_coq_045.v
@@ -29,7 +29,7 @@ Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A)
   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 *.
+  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_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index f47f9b5250..a14fb6aa57 100644
--- a/test-suite/bugs/opened/HoTT_coq_053.v
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -29,7 +29,7 @@ Definition IndiscreteCategory X : PreCategory
   := @Build_PreCategory X
                          (fun _ _ => Unit).
 
-Fail Definition NatCategory (n : nat) :=
+Definition NatCategory (n : nat) :=
   match n with
     | 0 => IndiscreteCategory Unit
     | _ => DiscreteCategory Bool
@@ -43,7 +43,7 @@ Definition NatCategory' (n : nat) :=
     | _ => DiscreteCategory Bool
   end.
 
-Fail Definition NatCategory'' (n : nat) :=
+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/closed/HoTT_coq_054.v
index fd37eb3300..f79fe1c1e7 100644
--- a/test-suite/bugs/opened/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/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.
 
-Fail Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
+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 @@ Fail 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).
-  Fail destruct x; destruct y; destruct pq; reflexivity.
-Fail Qed.
+  destruct x; destruct y; destruct pq; reflexivity.
+Qed.
 (* Toplevel input, characters 1367-1374:
 Error:
 In environment
diff --git a/test-suite/bugs/opened/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index 98e815aefc..fe9773ecd5 100644
--- a/test-suite/bugs/opened/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -180,8 +180,9 @@ Section bar.
 
   Variable D : PreCategory.
 
-  Fail Context `(has_colimits
+  Context `(has_colimits
             : forall F : Functor D C,
                 @IsColimit _ C D F (colimits F)).
 (* Error: Unsatisfied constraints: Top.3773 <= Set
  (maybe a bugged tactic). *)
+End bar.
diff --git a/test-suite/bugs/opened/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index a07f2f0fa2..fc15a88f7b 100644
--- a/test-suite/bugs/opened/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -50,7 +50,7 @@ Module failure.
   End SpecializedFunctor.
 
   Set Printing Universes.
-  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
   (* Toplevel input, characters 73-94:
 Error:
 The term "GraphIndexingCategory (* Top.563 *)" has type
@@ -58,6 +58,8 @@ The term "GraphIndexingCategory (* Top.563 *)" has type
 while it is expected to have type
  "SpecializedCategory (* Top.550 Top.551 *) ?7"
 (Universe inconsistency: Cannot enforce Set = Top.551)). *)
+  admit.
+  Defined.
 End failure.
 
 Module polycontext.
@@ -73,7 +75,7 @@ Module polycontext.
   End SpecializedFunctor.
 
   Set Printing Universes.
-  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
   (* Toplevel input, characters 73-94:
 Error:
 The term "GraphIndexingCategory (* Top.563 *)" has type
@@ -81,4 +83,6 @@ The term "GraphIndexingCategory (* Top.563 *)" has type
 while it is expected to have type
  "SpecializedCategory (* Top.550 Top.551 *) ?7"
 (Universe inconsistency: Cannot enforce Set = Top.551)). *)
+  admit.
+  Defined.
 End polycontext.
diff --git a/test-suite/bugs/opened/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v
index 9d87517e1c..71becfd2e5 100644
--- a/test-suite/bugs/opened/HoTT_coq_102.v
+++ b/test-suite/bugs/closed/HoTT_coq_102.v
@@ -23,5 +23,7 @@ Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A)
   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 *.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
   (* not convertible *)
+  admit.
+Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index f8b595d859..c3a83627ee 100644
--- a/test-suite/bugs/opened/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/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.
-  Fail refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
+  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_113.v b/test-suite/bugs/closed/HoTT_coq_113.v
index ae489e5f5b..3ef531bc96 100644
--- a/test-suite/bugs/opened/HoTT_coq_113.v
+++ b/test-suite/bugs/closed/HoTT_coq_113.v
@@ -12,7 +12,7 @@ Proof.
   admit.
 Defined.
 Definition foo := @Bar nat.
-Fail Check @foo Set.
+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_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
index f609aff5d7..63e3220c55 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.
 
-  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
+  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.
+    intro. (* Illegal application (Type Error) *)
+  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 2f8ec87491..3a8a2cf0c4 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -20,10 +20,9 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
 Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
 : FunctorToType C.
-  Fail refine (@Build_Functor _ C _ TypeCat
+  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
@@ -50,10 +49,12 @@ Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) :=
 Section SetGrothendieckCoercion.
   Context `(C : @Category objC).
   Variable F : Functor C SetCat.
-  Let F' := (F : FunctorToSet _) : FunctorToType _.
+  Fail 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.
-  Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
+  Fail 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_062.v b/test-suite/bugs/opened/HoTT_coq_062.v
index 99c2a1fb58..ce35818efd 100644
--- a/test-suite/bugs/opened/HoTT_coq_062.v
+++ b/test-suite/bugs/opened/HoTT_coq_062.v
@@ -70,7 +70,7 @@ Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
   intro f.
   Set Printing Universes.
   Set Printing All.
-  Fail pose proof (apD f (path_universe e)).
+  pose proof (apD f (path_universe e)).
   Fail pose proof (apD f p).
 (* Toplevel input, characters 18-19:
 Error: