Move closed bug 3314

1 files changed, 0 insertions, 146 deletions

diff --git a/test-suite/bugs/opened/3314.v b/test-suite/bugs/opened/3314.v
deleted file mode 100644
index 96b327e75a..0000000000
--- a/test-suite/bugs/opened/3314.v
+++ /dev/null
@@ -1,146 +0,0 @@
-Set Universe Polymorphism.
-Definition Lift
-: $(let U1 := constr:(Type) in
-    let U0 := constr:(Type : U1) in
-    exact (U0 -> U1))$
-  := fun T => T.
-
-Fail Check nat:Prop. (* The command has indeed failed with message:
-=> Error:
-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
-     : Prop
-(* Top.10
-   Top.9
-   Top.8 |= Top.10 < Top.9
-             Top.9 < Top.8
-             Top.9 <= Prop
-              *)
- *)
-Eval compute in Lift nat : Prop.
-(*      = nat
-     : Prop *)
-
-Section Hurkens.
-
-  Monomorphic Definition Type2 := Type.
-  Monomorphic Definition Type1 := Type : Type2.
-
-  (** Assumption of a retract from Type into Prop *)
-
-  Variable down : Type1 -> Prop.
-  Variable up : Prop -> Type1.
-
-  Hypothesis back : forall A, up (down A) -> A.
-
-  Hypothesis forth : forall A, A -> up (down A).
-
-  Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A),
-                           P (back A (forth A a)) -> P a.
-
-  Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A),
-                             P a -> P (back A (forth A a)).
-
-  (** Proof *)
-
-  Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
-  Definition U : Type1 := V -> Prop.
-
-  Definition sb (z:V) : V := fun A r a => r (z A r) a.
-  Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
-  Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x).
-  Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
-  Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))).
-  Definition I (x:U) : Prop :=
-    (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.
-
-  Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
-  Proof.
-    intros i y.
-    apply y.
-    unfold le, WF, induct.
-    apply forth.
-    intros x H0.
-    apply y.
-    unfold sb, le', le.
-    compute.
-    apply backforth_r.
-    exact H0.
-  Qed.
-
-  Lemma lemma1 : induct (fun u => down (I u)).
-  Proof.
-    unfold induct.
-    intros x p.
-    apply forth.
-    intro q.
-    generalize (q (fun u => down (I u)) p).
-    intro r.
-    apply back in r.
-    apply r.
-    intros i j.
-    unfold le, sb, le', le in j |-.
-                                apply backforth in j.
-    specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))).
-    apply q.
-    exact j.
-  Qed.
-
-  Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
-  Proof.
-    intro x.
-    generalize (x (fun u => down (I u)) lemma1).
-    intro r; apply back in r.
-    apply r.
-    intros i H0.
-    apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))).
-    unfold le, WF in H0.
-    apply back in H0.
-    exact H0.
-  Qed.
-
-  Theorem paradox : False.
-  Proof.
-    exact (lemma2 Omega).
-  Qed.
-
-End Hurkens.
-
-Definition informative (x : bool) :=
-  match x with
-    | true => Type
-    | false => Prop
-  end.
-
-Definition depsort (T : Type) (x : bool) : informative x :=
-  match x with
-    | true => T
-    | false => True
-  end.
-
-(** This definition should fail *)
-Definition Box (T : Type1) : Prop := Lift T.
-
-Definition prop {T : Type1} (t : Box T) : T := t.
-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.
-
-Definition forth (A : Type1) : A -> up (down A) := @wrap A.
-
-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) :
-      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.