From 347c4888e07cf76c7e1c6672ccfa89f86a0f11ea Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Oct 2014 13:46:56 +0200
Subject: Fix test-suite files which failed due to usage of $(admit)$ which now
 fails with Error: Already an existential evar of name Main

---
 test-suite/bugs/closed/3668.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'test-suite/bugs/closed/3668.v')

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.
-- 
cgit v1.2.3