diff options
| author | Matthieu Sozeau | 2014-10-15 13:46:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 13:46:56 +0200 |
| commit | 347c4888e07cf76c7e1c6672ccfa89f86a0f11ea (patch) | |
| tree | 083133886b1fa53fdcd064f6b98fa9f3a23004be /test-suite/bugs/closed/3668.v | |
| parent | 0307d06ac50caaa38d980a05f6ac3b0685720411 (diff) | |
Fix test-suite files which failed due to usage of $(admit)$ which
now fails with Error: Already an existential evar of name Main
Diffstat (limited to 'test-suite/bugs/closed/3668.v')
| -rw-r--r-- | test-suite/bugs/closed/3668.v | 5 |
1 files changed, 3 insertions, 2 deletions
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. |