Bug #3301 is closed, the projection cannot be defined anymore.

1 files changed, 1 insertions, 16 deletions

diff --git a/test-suite/bugs/opened/3301.v b/test-suite/bugs/closed/3301.v
index 955cfc3aa0..fca47b43c2 100644
--- a/test-suite/bugs/opened/3301.v
+++ b/test-suite/bugs/closed/3301.v
@@ -102,19 +102,4 @@ Record Box (T : Type) : Prop := wrap {prop : T}.
 Definition down (x : Type) : Prop := Box x.
 Definition up (x : Prop) : Type := x.
 
-Definition back A : up (down A) -> A := @prop A.
-
-Definition forth A : A -> up (down A) := wrap A.
-
-Definition backforth (A:Type) (P:A->Type) (a:A) :
-      P (back A (forth A a)) -> P a := fun H => H.
-
-Definition backforth_r (A:Type) (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).
-Qed.
-
-Print Assumptions pandora.
-(* Closed under the global context *)
+Fail Definition back A : up (down A) -> A := @prop A.