diff options
| -rw-r--r-- | test-suite/bugs/closed/3314.v (renamed from test-suite/bugs/opened/3314.v) | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/test-suite/bugs/opened/3314.v b/test-suite/bugs/closed/3314.v index 96b327e75a..647862637a 100644 --- a/test-suite/bugs/opened/3314.v +++ b/test-suite/bugs/closed/3314.v @@ -10,7 +10,7 @@ Fail Check nat:Prop. (* The command has indeed failed with message: The term "nat" has type "Set" while it is expected to have type "Prop". *) Set Printing All. Set Printing Universes. -Check Lift nat : Prop. (* Lift (* Top.8 Top.9 Top.10 *) nat:Prop +Fail Check Lift nat : Prop. (* Lift (* Top.8 Top.9 Top.10 *) nat:Prop : Prop (* Top.10 Top.9 @@ -19,7 +19,7 @@ Check Lift nat : Prop. (* Lift (* Top.8 Top.9 Top.10 *) nat:Prop Top.9 <= Prop *) *) -Eval compute in Lift nat : Prop. +Fail Eval compute in Lift nat : Prop. (* = nat : Prop *) @@ -129,18 +129,19 @@ Definition wrap {T : Type1} (t : T) : Box T := t. Definition down (x : Type1) : Prop := Box x. Definition up (x : Prop) : Type1 := x. -Definition back A : up (down A) -> A := @prop A. +Fail Definition back A : up (down A) -> A := @prop A. -Definition forth (A : Type1) : A -> up (down A) := @wrap A. +Fail Definition forth (A : Type1) : A -> up (down A) := @wrap A. -Definition backforth (A:Type1) (P:A->Type) (a:A) : +Fail Definition backforth (A:Type1) (P:A->Type) (a:A) : P (back A (forth A a)) -> P a := fun H => H. -Definition backforth_r (A:Type1) (P:A->Type) (a:A) : +Fail Definition backforth_r (A:Type1) (P:A->Type) (a:A) : P a -> P (back A (forth A a)) := fun H => H. Theorem pandora : False. - apply (paradox down up back forth backforth backforth_r). + Fail apply (paradox down up back forth backforth backforth_r). + admit. Qed. Print Assumptions pandora. |