Fix test-suite files which failed due to usage of $(admit)$ which

now fails with Error: Already an existential evar of name Main

2 files changed, 5 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v
index 1256d125f5..ba6006ed93 100644
--- a/test-suite/bugs/closed/3648.v
+++ b/test-suite/bugs/closed/3648.v
@@ -49,13 +49,11 @@ Record Functor (C D : PreCategory) :=
   }.
 Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
 Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
-
+Axiom cheat : forall {A}, A.
 Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
 Definition functor_category (C D : PreCategory) : PreCategory.
   exact (@Build_PreCategory (Functor C D)
-                            (@NaturalTransformation C D)
-                            $(admit)$
-                            $(admit)$).
+                            (@NaturalTransformation C D) cheat cheat).
 Defined.
 
 Local Notation "C -> D" := (functor_category C D) : category_scope.
diff --git a/test-suite/bugs/closed/3668.v b/test-suite/bugs/closed/3668.v
index ec70fc5abe..547159b954 100644
--- a/test-suite/bugs/closed/3668.v
+++ b/test-suite/bugs/closed/3668.v
@@ -11,12 +11,13 @@ Axiom IsHProp : Type -> Type.
 Inductive Bool := true | false.
 Definition negb (b : Bool) := if b then false else true.
 Hypothesis LEM : forall A : Type, IsHProp A -> A + (A -> False).
+Axiom cheat : forall {A},A.
 Module NonPrim.
   Class Contr (A : Type) := { center : A ; contr : (forall y : A, center = y) }.
   Definition Book_6_9 : forall X, X -> X.
   Proof.
     intro X.
-    pose proof (@LEM (Contr { f : X <~> X & ~(forall x, f x = x) }) $(admit)$) as contrXEquiv.
+    pose proof (@LEM (Contr { f : X <~> X & ~(forall x, f x = x) }) cheat) as contrXEquiv.
     destruct contrXEquiv as [[f H]|H]; [ exact f.1 | exact (fun x => x) ].
   Defined.
   Lemma Book_6_9_not_id b : Book_6_9 Bool b = negb b.
@@ -36,7 +37,7 @@ Module Prim.
   Definition Book_6_9 : forall X, X -> X.
   Proof.
     intro X.
-    pose proof (@LEM (Contr { f : X <~> X & ~(forall x, f x = x) }) $(admit)$) as contrXEquiv.
+    pose proof (@LEM (Contr { f : X <~> X & ~(forall x, f x = x) }) cheat) as contrXEquiv.
     destruct contrXEquiv as [[f H]|H]; [ exact (f.1) | exact (fun x => x) ].
   Defined.
   Lemma Book_6_9_not_id b : Book_6_9 Bool b = negb b.