From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 21 Sep 2015 11:55:32 +0200
Subject: Forcing i > Set for global universes (incomplete)

---
 test-suite/bugs/closed/3309.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 980431576c..6e97ed2afe 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -117,7 +117,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a
 Defined.
 
 Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X }  : iseqclass R A -> ishinh ( carrier A ) .
-intros X R A; exact ( fun is : iseqclass R A =>  projT1' _ is ).
+intros X R A. exact (fun is : iseqclass R A => projT1' _ is ).
 Defined.
 
 Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) .
@@ -141,7 +141,7 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f.
   admit.
 Defined.
 
-Definition setquot { X : UU } ( R : hrel X ) : Type.
+Definition setquot { X : UU } ( R : hrel X ) : Set.
 intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ).
 Defined.
 Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R.
@@ -157,7 +157,7 @@ Definition setquotinset { X : UU } ( R : hrel X ) : hSet.
 intros; exact ( hSetpair (setquot R) admit) .
 Defined.
 
-Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
+Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
 intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _  ( projT2' _ cd ) ) ) ).
 Defined.
 
-- 
cgit v1.2.3


From 91e01278de2420a64f1c8de03c0bc6e614577042 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 18:53:35 +0200
Subject: Univs: fixed bug #4328.

---
 test-suite/bugs/closed/4328.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4328.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v
new file mode 100644
index 0000000000..8e1bb31007
--- /dev/null
+++ b/test-suite/bugs/closed/4328.v
@@ -0,0 +1,6 @@
+Inductive M (A:Type) : Type := M'.
+Axiom pi : forall (P : Prop) (p : P), Prop.
+Definition test1 A (x : _) := pi A x.           (* success     *)
+Fail Definition test2 A (x : A) := pi A x.           (* failure ??? *)
+Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure     *)
+Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file
-- 
cgit v1.2.3


From 43858a207437fa08f066bdd3cae7bcd3034808f1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 19:14:05 +0200
Subject: Univs: fix Universe vernacular, fix bug #4287.

No universe can be set lower than Prop anymore (or Set).
---
 test-suite/bugs/closed/4287.v | 172 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 172 insertions(+)
 create mode 100644 test-suite/bugs/closed/4287.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
new file mode 100644
index 0000000000..732f19f33c
--- /dev/null
+++ b/test-suite/bugs/closed/4287.v
@@ -0,0 +1,172 @@
+
+Universe b.
+
+Universe c.
+
+Definition U : Type@{b} := Type@{c}.
+
+Module Type MT.
+
+Definition T := Prop.
+End MT.
+
+Module M : MT.
+   Definition T := Type@{b}.
+
+Print Universes.
+Fail End M.
+
+Set Universe Polymorphism.
+
+(* This is a modified version of Hurkens with all universes floating *)
+Section Hurkens.
+
+Variable down : Type -> Type.
+Variable up : Type -> Type.
+
+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 : Type := forall A:Type, ((up A -> Type) -> up A -> Type) -> up A -> Type.
+Definition U : Type := V -> Type.
+
+Definition sb (z:V) : V := fun A r a => r (z A r) a.
+Definition le (i:U -> Type) (x:U) : Type := x (fun A r a => i (fun v => sb v A r a)).
+Definition le' (i:up (down U) -> Type) (x:up (down U)) : Type := le (fun a:U => i (forth _ a)) (back _ x).
+Definition induct (i:U -> Type) : Type := 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) : Type :=
+  (forall i:U -> Type, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.
+
+Lemma Omega : forall i:U -> Type, 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 -> Type, 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.
+
+Polymorphic Record box (T : Type) := wrap {unwrap : T}.
+
+(* Here we instantiate to Prop *)
+(* Here we instantiate to Prop *)
+
+Fail Definition down (x : Type) : Set := box x.
+Definition down (x : Set) : Set := box x.
+Definition up (x : Prop) : Type := x.
+
+Fail Definition back A : up (down A) -> A := unwrap A.
+
+Fail Definition forth A : A -> up (down A) := wrap A.
+
+(* Lemma backforth (A:Type) (P:A->Type) (a:A) : *)
+(*       P (back A (forth A a)) -> P a. *)
+(* Proof. *)
+(* intros; assumption. *)
+(* Qed. *)
+
+(* Lemma backforth_r (A:Type) (P:A->Type) (a:A) : *)
+(*       P a -> P (back A (forth A a)). *)
+(* Proof. *)
+(* intros; assumption. *)
+(* Qed. *)
+
+(* Theorem bad : False. *)
+(* apply (paradox down up back forth backforth backforth_r). *)
+(* Qed. *)
+
+(* Print Assumptions bad. *)
+
+Definition id {A : Type} (a : A) := a.
+Definition setlt (A : Type@{i}) :=
+  let foo := Type@{i} : Type@{j} in True.
+
+Definition setle (B : Type@{i}) :=
+  let foo (A : Type@{j}) := A in foo B.
+
+Fail Check @setlt@{j Prop}.
+Check @setlt@{Prop j}.
+Check @setle@{Prop j}.
+
+Fail Definition foo := @setle@{j Prop}.
+Definition foo := @setle@{Prop j}.
+
+(* Definition up (x : Prop) : Type := x. *)
+
+(* Definition back A : up (down A) -> A := unwrap A. *)
+
+(* Definition forth A : A -> up (down A) := wrap A. *)
+
+(* Lemma backforth (A:Type) (P:A->Type) (a:A) : *)
+(*       P (back A (forth A a)) -> P a. *)
+(* Proof. *)
+(* intros; assumption. *)
+(* Qed. *)
+
+(* Lemma backforth_r (A:Type) (P:A->Type) (a:A) : *)
+(*       P a -> P (back A (forth A a)). *)
+(* Proof. *)
+(* intros; assumption. *)
+(* Qed. *)
+
+(* Theorem bad : False. *)
+(* apply (paradox down up back forth backforth backforth_r). *)
+(* Qed. *)
+
+(* Print Assumptions bad. *)
+
+(* Polymorphic Record box (T : Type) := wrap {unwrap : T}. *)
+
+(* Definition down (x : Type) : Prop := box x. *)
-- 
cgit v1.2.3


From b969b459021fe70272baa85e83c12268baf13836 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 19:31:18 +0200
Subject: Univs: fixed bug 2584, correct universe found for mutual inductive.

---
 test-suite/bugs/closed/2584.v | 89 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 test-suite/bugs/closed/2584.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
new file mode 100644
index 0000000000..a5f4ae64a0
--- /dev/null
+++ b/test-suite/bugs/closed/2584.v
@@ -0,0 +1,89 @@
+Require Import List.
+
+Set Implicit Arguments.
+
+Definition err : Type := unit. 
+
+Inductive res (A: Type) : Type :=
+| OK: A -> res A
+| Error: err -> res A. 
+
+Implicit Arguments Error [A].
+
+Set Printing Universes.
+
+Section FOO.
+
+Inductive ftyp : Type :=
+  | Funit : ftyp 
+  | Ffun : list ftyp -> ftyp 
+  | Fref : area -> ftyp
+with area : Type := 
+  | Stored : ftyp -> area        
+.
+
+Print ftyp.
+(* yields:
+Inductive ftyp : Type (* Top.27429 *) :=
+    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
+  with area : Type (* Set *) :=  Stored : ftyp -> area
+*)
+
+Fixpoint tc_wf_type (ftype: ftyp) {struct ftype}: res unit :=
+  match ftype with
+    | Funit => OK tt
+    | Ffun args => 
+       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
+           match ftypes with
+             | nil => OK tt
+             | t::ts =>
+                 match tc_wf_type t with
+                   | OK tt => tc_wf_types ts
+                   | Error m => Error m 
+                 end 
+           end) args) 
+     | Fref a => tc_wf_area a
+   end
+with tc_wf_area (ar:area): res unit :=
+  match ar with
+    | Stored c => tc_wf_type c
+  end.
+
+End FOO.
+
+Print ftyp.
+(* yields:
+Inductive ftyp : Type (* Top.27465 *) :=
+    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
+  with area : Set :=  Stored : ftyp -> area
+*)
+
+Fixpoint tc_wf_type' (ftype: ftyp) {struct ftype}: res unit :=
+  match ftype with
+    | Funit => OK tt
+    | Ffun args => 
+       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
+           match ftypes with
+             | nil => OK tt
+             | t::ts =>
+                 match tc_wf_type' t with
+                   | OK tt => tc_wf_types ts
+                   | Error m => Error m 
+                 end 
+           end) args) 
+     | Fref a => tc_wf_area' a
+   end
+with tc_wf_area' (ar:area): res unit :=
+  match ar with
+    | Stored c => tc_wf_type' c
+  end.
+
+(* yields:
+Error:
+Incorrect elimination of "ar" in the inductive type "area":
+the return type has sort "Type (* max(Set, Top.27424) *)" while it
+should be "Prop" or "Set".
+Elimination of an inductive object of sort Set
+is not allowed on a predicate in sort Type
+because strong elimination on non-small inductive types leads to paradoxes.
+*)
\ No newline at end of file
-- 
cgit v1.2.3


From e51f708ac911f376f09297cad7d7d27510fe8990 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 15:30:43 +0200
Subject: Fix test-suite file: failing earlier as expected.

---
 test-suite/bugs/closed/3314.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index e63c46da04..fb3791af55 100644
--- a/test-suite/bugs/closed/3314.v
+++ b/test-suite/bugs/closed/3314.v
@@ -122,12 +122,12 @@ Definition depsort (T : Type) (x : bool) : informative x :=
   end.
 
 (** This definition should fail *)
-Definition Box (T : Type1) : Prop := Lift T.
+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.
+Fail Definition prop {T : Type1} (t : Box T) : T := t.
+Fail Definition wrap {T : Type1} (t : T) : Box T := t.
 
-Definition down (x : Type1) : Prop := Box x.
+Fail Definition down (x : Type1) : Prop := Box x.
 Definition up (x : Prop) : Type1 := x.
 
 Fail Definition back A : up (down A) -> A := @prop A.
-- 
cgit v1.2.3


From 96760d8516398ecfa55e4e6f808dd6aa5305e483 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 17:57:37 +0200
Subject: Fix test-suite file for bug #3777

---
 test-suite/bugs/closed/3777.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/bugs/closed/3777.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
new file mode 100644
index 0000000000..b9b2dd6b3e
--- /dev/null
+++ b/test-suite/bugs/closed/3777.v
@@ -0,0 +1,16 @@
+Module WithoutPoly.
+  Unset Universe Polymorphism.
+  Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
+  Set Printing Universes.
+  Definition bla := ((@foo : Set -> _ -> _) : _ -> Type -> _).
+  (* ((fun A : Set => foo A):Set -> Type@{Top.55} -> Type@{Top.55})
+:Set -> Type@{Top.55} -> Type@{Top.55}
+     : Set -> Type@{Top.55} -> Type@{Top.55}
+(*  |= Set <= Top.55
+         *) *)
+End WithoutPoly.
+Module WithPoly.
+  Set Universe Polymorphism.
+  Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
+  Set Printing Universes.
+  Fail Check ((@foo : Set -> _ -> _) : _ -> Type -> _).
-- 
cgit v1.2.3


From 856a61c1b3c5ee2b4dec08809e5e916d8954d5f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:13:28 +0200
Subject: Univs: test-suite file for #4301, subtyping of poly parameters

---
 test-suite/bugs/closed/4301.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/4301.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
new file mode 100644
index 0000000000..1a8d3611bf
--- /dev/null
+++ b/test-suite/bugs/closed/4301.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Parameter U : Type.
+End Foo.
+
+(* Module Lower (X : Foo). *)
+(*   Definition U' : Prop := X.U@{Prop}. *)
+(* End Lower. *)
+(* Module Lower (X : Foo with Definition U := Prop). *)
+(*   Definition U' := X.U@{Prop}. *)
+(* End Lower. *)
+Module Lower (X : Foo with Definition U := True).
+  (* Definition U' : Prop := X.U. *)
+End Lower.
+
+Module M : Foo.
+  Definition U := nat : Type@{i}. 
+End M.
-- 
cgit v1.2.3


From 816f03befa9264cd90e57c75be93f568b90ae180 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:16:19 +0200
Subject: Univs: test-suite file for bug #2016

---
 test-suite/bugs/closed/2016.v | 62 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 test-suite/bugs/closed/2016.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
new file mode 100644
index 0000000000..13ec5bea9b
--- /dev/null
+++ b/test-suite/bugs/closed/2016.v
@@ -0,0 +1,62 @@
+(* Coq 8.2beta4 *)
+Require Import Classical_Prop. 
+
+Record coreSemantics : Type := CoreSemantics {
+  core: Type;
+  corestep: core ->  core -> Prop;
+  corestep_fun: forall q q1 q2, corestep q q1 -> corestep q q2 -> q1 = q2
+}.
+
+Definition state : Type := {sem: coreSemantics & sem.(core)}.
+
+Inductive step: state -> state -> Prop :=
+  | step_core: forall sem st st'
+             (Hcs: sem.(corestep) st st'),
+             step (existT _ sem st) (existT _ sem st').
+
+Lemma step_fun: forall st1 st2 st2', step st1 st2 -> step st1 st2' -> st2 = st2'.
+Proof.
+intros.
+inversion H; clear H; subst. inversion H0; clear H0; subst; auto.
+generalize (inj_pairT2 _ _ _ _ _ H2); clear H2; intro; subst.
+rewrite (corestep_fun _ _ _ _ Hcs Hcs0); auto.
+Qed.
+
+Record oe_core := oe_Core {
+    in_core: Type;
+    in_corestep: in_core -> in_core -> Prop;
+    in_corestep_fun: forall q  q1 q2,  in_corestep q q1 -> in_corestep q q2 -> q1 = q2;
+   in_q: in_core
+}.
+
+Definition oe2coreSem (oec : oe_core) : coreSemantics :=
+  CoreSemantics oec.(in_core) oec.(in_corestep)  oec.(in_corestep_fun).
+
+Definition oe_corestep (q q': oe_core) :=
+    step (existT _ (oe2coreSem q) q.(in_q)) (existT _ (oe2coreSem q') q'.(in_q)).
+
+Lemma inj_pairT1: forall (U: Type) (P: U -> Type) (p1 p2: U) x y,
+      existT P p1 x = existT P p2 y -> p1=p2.
+Proof. intros; injection H; auto.
+Qed.
+
+Definition f := CoreSemantics oe_core.
+
+Lemma oe_corestep_fun: forall q q1 q2, 
+       oe_corestep q q1 -> oe_corestep q q2 -> q1 = q2.
+Proof.
+unfold oe_corestep; intros.
+assert (HH:= step_fun _ _ _ H H0); clear H H0.
+destruct q1; destruct q2; unfold oe2coreSem; simpl in *.
+generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros.
+injection H; clear H; intros.
+revert in_q1  in_corestep1 in_corestep_fun1
+          H.
+pattern in_core1.
+apply eq_ind_r with (x := in_core0).
+admit.
+apply sym_eq.
+(** good to here **)
+Show Universes.
+Print Universes.
+Fail apply H0.
\ No newline at end of file
-- 
cgit v1.2.3


From 4b51494ef6fee2301766fb4a44020dc2ad95799f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:20:33 +0200
Subject: Univs: fix test-suite file for HoTT/coq bug #120

---
 test-suite/bugs/closed/HoTT_coq_120.v | 138 ++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_120.v | 137 ---------------------------------
 2 files changed, 138 insertions(+), 137 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_120.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_120.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
new file mode 100644
index 0000000000..e46ea58bb3
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -0,0 +1,138 @@
+Require Import TestSuite.admit.
+(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
+Set Universe Polymorphism.
+Generalizable All Variables.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+
+Class Contr_internal (A : Type) := BuildContr {
+                                       center : A ;
+                                       contr : (forall y : A, center = y)
+                                     }.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+  := match n with
+       | 0 => trunc_S (trunc_S minus_two)
+       | S n' => trunc_S (nat_to_trunc_index n')
+     end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Notation minus_one:=(trunc_S minus_two).
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc minus_two).
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext := {}.
+Inductive Unit : Set := tt.
+
+Instance contr_unit : Contr Unit | 0 := let x := {|
+                                              center := tt;
+                                              contr := fun t : Unit => match t with tt => idpath end
+                                            |} in x.
+Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
+admit.
+Defined.
+Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+Definition Unit_hp:hProp:=(hp Unit _).
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+Definition ismono {X Y} (f : X -> Y)
+  := forall Z : hSet,
+     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.
+
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory :=
+  Build_PreCategory {
+      object :> Type;
+      morphism : object -> object -> Type;
+      compose : forall s d d', morphism d d' -> morphism s d -> morphism s d'
+    }.
+Arguments compose [!C s d d'] m1 m2 : rename.
+
+Infix "o" := compose : morphism_scope.
+Local Open Scope morphism_scope.
+
+Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
+  is_epimorphism : forall z (m1 m2 : morphism C y z),
+                     m1 o m = m2 o m
+                     -> m1 = m2.
+
+Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
+  is_monomorphism : forall z (m1 m2 : morphism C z x),
+                      m o m1 = m o m2
+                      -> m1 = m2.
+Class Univalence := {}.
+Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted.
+
+Definition set_cat : PreCategory
+  := @Build_PreCategory hSet
+                        (fun x y => forall _ : x, y)%core
+                        (fun _ _ _ f g x => f (g x))%core.
+Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
+Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
+Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
+Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
+                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
+Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
+Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f.
+Proof.
+  intros epif y.
+  set (g :=fun _:Y => Unit_hp).
+  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
+  clear fs'.
+  hnf in epif.
+  specialize (epif (BuildhSet hProp _) g h).
+  admit.
+Defined.
+Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f)
+: IsEquiv f.
+Proof.
+  pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf.
+  admit.
+Defined.
+Section fully_faithful_helpers.
+  Context `{fs0 : Funext}.
+  Variables x y : hSet.
+  Variable m : x -> y.
+
+  Fail Let isequiv_isepi_ismono_helper ua :=
+    (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).
+
+  Goal True.
+  Fail set (isequiv_isepimorphism_ismonomorphism
+       := fun `{Univalence}
+              (Hepi : IsEpimorphism (m : morphism set_cat x y))
+              (Hmono : IsMonomorphism (m : morphism set_cat x y))
+          => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
+  admit.
+  Undo.
+  Fail set (isequiv_isepimorphism_ismonomorphism
+       := fun `{Univalence}
+              (Hepi : IsEpimorphism (m : morphism set_cat x y))
+              (Hmono : IsMonomorphism (m : morphism set_cat x y))
+          => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono)
+              : @IsEquiv _ _ m)).
+  Set Printing Universes.
+  admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
+< Top.235). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
deleted file mode 100644
index 05ee6c7b60..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ /dev/null
@@ -1,137 +0,0 @@
-Require Import TestSuite.admit.
-(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
-Set Universe Polymorphism.
-Generalizable All Variables.
-Reserved Notation "g 'o' f" (at level 40, left associativity).
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-
-Class IsEquiv {A B : Type} (f : A -> B) := {}.
-
-Class Contr_internal (A : Type) := BuildContr {
-                                       center : A ;
-                                       contr : (forall y : A, center = y)
-                                     }.
-
-Inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index -> trunc_index.
-
-Fixpoint nat_to_trunc_index (n : nat) : trunc_index
-  := match n with
-       | 0 => trunc_S (trunc_S minus_two)
-       | S n' => trunc_S (nat_to_trunc_index n')
-     end.
-
-Coercion nat_to_trunc_index : nat >-> trunc_index.
-
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
-  match n with
-    | minus_two => Contr_internal A
-    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
-  end.
-
-Notation minus_one:=(trunc_S minus_two).
-
-Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
-
-Notation Contr := (IsTrunc minus_two).
-Notation IsHProp := (IsTrunc minus_one).
-Notation IsHSet := (IsTrunc 0).
-
-Class Funext := {}.
-Inductive Unit : Set := tt.
-
-Instance contr_unit : Contr Unit | 0 := let x := {|
-                                              center := tt;
-                                              contr := fun t : Unit => match t with tt => idpath end
-                                            |} in x.
-Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
-admit.
-Defined.
-Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
-Definition Unit_hp:hProp:=(hp Unit _).
-Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
-Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-Definition ismono {X Y} (f : X -> Y)
-  := forall Z : hSet,
-     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.
-
-Delimit Scope morphism_scope with morphism.
-Delimit Scope category_scope with category.
-Delimit Scope object_scope with object.
-Record PreCategory :=
-  Build_PreCategory {
-      object :> Type;
-      morphism : object -> object -> Type;
-      compose : forall s d d', morphism d d' -> morphism s d -> morphism s d'
-    }.
-Arguments compose [!C s d d'] m1 m2 : rename.
-
-Infix "o" := compose : morphism_scope.
-Local Open Scope morphism_scope.
-
-Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
-  is_epimorphism : forall z (m1 m2 : morphism C y z),
-                     m1 o m = m2 o m
-                     -> m1 = m2.
-
-Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
-  is_monomorphism : forall z (m1 m2 : morphism C z x),
-                      m o m1 = m o m2
-                      -> m1 = m2.
-Class Univalence := {}.
-Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted.
-
-Definition set_cat : PreCategory
-  := @Build_PreCategory hSet
-                        (fun x y => forall _ : x, y)%core
-                        (fun _ _ _ f g x => f (g x))%core.
-Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
-Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
-Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
-Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
-                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
-Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
-Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f.
-Proof.
-  intros epif y.
-  set (g :=fun _:Y => Unit_hp).
-  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
-  clear fs'.
-  hnf in epif.
-  specialize (epif (BuildhSet hProp _) g h).
-  admit.
-Defined.
-Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f)
-: IsEquiv f.
-Proof.
-  pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf.
-  admit.
-Defined.
-Section fully_faithful_helpers.
-  Context `{fs0 : Funext}.
-  Variables x y : hSet.
-  Variable m : x -> y.
-
-  Let isequiv_isepi_ismono_helper ua := (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).
-
-  Goal True.
-  Fail set (isequiv_isepimorphism_ismonomorphism
-       := fun `{Univalence}
-              (Hepi : IsEpimorphism (m : morphism set_cat x y))
-              (Hmono : IsMonomorphism (m : morphism set_cat x y))
-          => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
-  admit.
-  Undo.
-  Fail set (isequiv_isepimorphism_ismonomorphism'
-       := fun `{Univalence}
-              (Hepi : IsEpimorphism (m : morphism set_cat x y))
-              (Hmono : IsMonomorphism (m : morphism set_cat x y))
-          => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono)
-              : @IsEquiv _ _ m)).
-  Set Printing Universes.
-  admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
-< Top.235). *)
-- 
cgit v1.2.3


From 07e96102047f55be45bcb2e0a72ac3c764e398b1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:40:20 +0200
Subject: Univs: minor fixes to test-suite files

108 used an implicit lowering to Prop.
---
 test-suite/bugs/closed/HoTT_coq_053.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_093.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_108.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index a14fb6aa57..e2bf1dbedb 100644
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -39,7 +39,7 @@ Definition NatCategory (n : nat) :=
 Definition NatCategory' (n : nat) :=
   match n with
     | 0 => (fun X => @Build_PreCategory X
-                         (fun _ _ => Unit : Prop)) Unit
+                         (fun _ _ => Unit : Set)) Unit
     | _ => DiscreteCategory Bool
   end.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index 38943ab353..f382dac976 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -21,7 +21,7 @@ Section lift.
   Definition Lift (A : Type@{i}) : Type@{j} := A.
 End lift.
 
-Goal forall (A : Type@{i}) (x y : A), @paths@{i} A x y -> @paths@{j} A x y.
+Goal forall (A : Type@{i}) (x y : A), @paths@{i j} A x y -> @paths@{j k} A x y.
 intros A x y p.
 compute in *. destruct p. exact idpath.
 Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index 4f5ef99740..b6c0da76ba 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -107,7 +107,7 @@ Section path_functor.
   Variable D : PreCategory.
   Local Notation path_functor'_T F G
     := { HO : object_of F = object_of G
-       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
+       & transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                    HO
                    (morphism_of F)
          = morphism_of G }
-- 
cgit v1.2.3


From 67bdc25eb69ecd485ae1c8fa2dd71d1933f355d0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 19:05:47 +0200
Subject: Univs: fixed 3685 by side-effect :)

---
 test-suite/bugs/closed/3685.v | 75 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3685.v | 75 -------------------------------------------
 2 files changed, 75 insertions(+), 75 deletions(-)
 create mode 100644 test-suite/bugs/closed/3685.v
 delete mode 100644 test-suite/bugs/opened/3685.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
new file mode 100644
index 0000000000..a5bea34a98
--- /dev/null
+++ b/test-suite/bugs/closed/3685.v
@@ -0,0 +1,75 @@
+Require Import TestSuite.admit.
+Set Universe Polymorphism.
+Class Funext := { }.
+Delimit Scope category_scope with category.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Set Implicit Arguments.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
+    identity_of : forall s m, morphism_of s s m = morphism_of s s m }.
+Definition sub_pre_cat `{Funext} (P : PreCategory -> Type) : PreCategory.
+Proof.
+  exact (@Build_PreCategory PreCategory Functor).
+Defined.
+Definition opposite (C : PreCategory) : PreCategory.
+Proof.
+  exact (@Build_PreCategory C (fun s d => morphism C d s)).
+Defined.
+Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope.
+Definition prod (C D : PreCategory) : PreCategory.
+Proof.
+  refine (@Build_PreCategory
+            (C * D)%type
+            (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)).
+Defined.
+Local Infix "*" := prod : category_scope.
+Record NaturalTransformation C D (F G : Functor C D) := {}.
+Definition functor_category (C D : PreCategory) : PreCategory.
+Proof.
+  exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)).
+Defined.
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Module Export PointwiseCore.
+  Local Open Scope category_scope.
+  Definition pointwise
+             (C C' : PreCategory)
+             (F : Functor C' C)
+             (D D' : PreCategory)
+             (G : Functor D D')
+  : Functor (C -> D) (C' -> D').
+  Proof.
+    refine (Build_Functor
+              (C -> D) (C' -> D')
+              _
+              _
+              _);
+    abstract admit.
+  Defined.
+End PointwiseCore.
+Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G.
+Local Open Scope category_scope.
+Module Success.
+  Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
+             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
+  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
+    := Eval cbv zeta in
+        let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => @Pidentity_of _ _ _ _).
+End Success.
+Module Bad.
+  Include PointwiseCore.
+  Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
+             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
+  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
+    := Eval cbv zeta in
+        let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => @Pidentity_of _ _ _ _).
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
deleted file mode 100644
index b2b5db6be7..0000000000
--- a/test-suite/bugs/opened/3685.v
+++ /dev/null
@@ -1,75 +0,0 @@
-Require Import TestSuite.admit.
-Set Universe Polymorphism.
-Class Funext := { }.
-Delimit Scope category_scope with category.
-Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
-Set Implicit Arguments.
-Record Functor (C D : PreCategory) :=
-  { object_of :> C -> D;
-    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
-    identity_of : forall s m, morphism_of s s m = morphism_of s s m }.
-Definition sub_pre_cat `{Funext} (P : PreCategory -> Type) : PreCategory.
-Proof.
-  exact (@Build_PreCategory PreCategory Functor).
-Defined.
-Definition opposite (C : PreCategory) : PreCategory.
-Proof.
-  exact (@Build_PreCategory C (fun s d => morphism C d s)).
-Defined.
-Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope.
-Definition prod (C D : PreCategory) : PreCategory.
-Proof.
-  refine (@Build_PreCategory
-            (C * D)%type
-            (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)).
-Defined.
-Local Infix "*" := prod : category_scope.
-Record NaturalTransformation C D (F G : Functor C D) := {}.
-Definition functor_category (C D : PreCategory) : PreCategory.
-Proof.
-  exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)).
-Defined.
-Local Notation "C -> D" := (functor_category C D) : category_scope.
-Module Export PointwiseCore.
-  Local Open Scope category_scope.
-  Definition pointwise
-             (C C' : PreCategory)
-             (F : Functor C' C)
-             (D D' : PreCategory)
-             (G : Functor D D')
-  : Functor (C -> D) (C' -> D').
-  Proof.
-    refine (Build_Functor
-              (C -> D) (C' -> D')
-              _
-              _
-              _);
-    abstract admit.
-  Defined.
-End PointwiseCore.
-Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G.
-Local Open Scope category_scope.
-Module Success.
-  Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
-             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
-  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
-    := Eval cbv zeta in
-        let object_of := (fun CD => (((fst CD) -> (snd CD))))
-        in Build_Functor
-             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
-             object_of
-             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
-             (fun _ _ => @Pidentity_of _ _ _ _).
-End Success.
-Module Bad.
-  Include PointwiseCore.
-  Fail Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
-             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
-  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
-    := Eval cbv zeta in
-        let object_of := (fun CD => (((fst CD) -> (snd CD))))
-        in Build_Functor
-             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
-             object_of
-             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
-             (fun _ _ => @Pidentity_of _ _ _ _).
-- 
cgit v1.2.3


From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:36:57 +0200
Subject: Univs: fix bug #4251, handling of template polymorphic constants.

---
 test-suite/bugs/closed/4251.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/4251.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v
new file mode 100644
index 0000000000..66343d6671
--- /dev/null
+++ b/test-suite/bugs/closed/4251.v
@@ -0,0 +1,17 @@
+
+Inductive array : Type -> Type :=
+| carray : forall A, array A.
+
+Inductive Mtac : Type -> Prop :=
+| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B
+| array_make : forall {A}, A -> Mtac (array A).
+
+Definition Ref := array.
+
+Definition ref : forall {A}, A -> Mtac (Ref A) := 
+  fun A x=> array_make x.
+Check array Type.
+Check fun A : Type => Ref A.
+
+Definition abs_val (a : Type) :=
+  bind (ref a) (fun r : array Type => array_make tt).
\ No newline at end of file
-- 
cgit v1.2.3


From d4869e059bfb73d99e1f5ef1b0a1f0906fa27056 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:40:17 +0200
Subject: Univs: correct handling of with in modules

For polymorphic and non-polymorphic parameters and definitions, fixes
bugs #4298, #4294
---
 test-suite/bugs/closed/4294.v | 31 +++++++++++++++++++++++++++++++
 test-suite/bugs/closed/4298.v |  7 +++++++
 2 files changed, 38 insertions(+)
 create mode 100644 test-suite/bugs/closed/4294.v
 create mode 100644 test-suite/bugs/closed/4298.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4294.v b/test-suite/bugs/closed/4294.v
new file mode 100644
index 0000000000..1d5e3c71b8
--- /dev/null
+++ b/test-suite/bugs/closed/4294.v
@@ -0,0 +1,31 @@
+Require Import Hurkens.
+
+Module NonPoly.
+Module Type Foo.
+  Definition U := Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type.
+  Definition U := Type.
+  Definition eq : Type = U := eq_refl.
+End M.
+
+Print Universes.
+Fail Definition bad : False := TypeNeqSmallType.paradox M.U M.eq.
+End NonPoly.
+
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type.
+  Monomorphic Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type.
+  Definition U := Type.
+  Monomorphic Definition eq : Type = U := eq_refl.
+End M.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox Type M.eq.
+(* Print Assumptions bad. *)
diff --git a/test-suite/bugs/closed/4298.v b/test-suite/bugs/closed/4298.v
new file mode 100644
index 0000000000..875612ddf4
--- /dev/null
+++ b/test-suite/bugs/closed/4298.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type.
+End Foo.
+
+Fail Module M : Foo with Definition U := Prop.
-- 
cgit v1.2.3


From f4db3d72abc1872839bcacd3b28a439e69d0a2e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:41:23 +0200
Subject: Univs: fix test-suite file (4301 is invalid, but a good regression
 test)

---
 test-suite/bugs/closed/4301.v | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
index 1a8d3611bf..3b00efb213 100644
--- a/test-suite/bugs/closed/4301.v
+++ b/test-suite/bugs/closed/4301.v
@@ -4,14 +4,7 @@ Module Type Foo.
   Parameter U : Type.
 End Foo.
 
-(* Module Lower (X : Foo). *)
-(*   Definition U' : Prop := X.U@{Prop}. *)
-(* End Lower. *)
-(* Module Lower (X : Foo with Definition U := Prop). *)
-(*   Definition U' := X.U@{Prop}. *)
-(* End Lower. *)
-Module Lower (X : Foo with Definition U := True).
-  (* Definition U' : Prop := X.U. *)
+Module Lower (X : Foo with Definition U := True : Type).
 End Lower.
 
 Module M : Foo.
-- 
cgit v1.2.3


From cbcf55ca44b5374f39979ced88061c82c03901b3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:42:39 +0200
Subject: Univs: Remove test-suite file #3309

This relied on universes lower than Prop. A proper test
for the sharing option should be found, -type-in-type is not
enough either.
---
 test-suite/bugs/closed/3309.v | 334 ------------------------------------------
 1 file changed, 334 deletions(-)
 delete mode 100644 test-suite/bugs/closed/3309.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
deleted file mode 100644
index 6e97ed2afe..0000000000
--- a/test-suite/bugs/closed/3309.v
+++ /dev/null
@@ -1,334 +0,0 @@
-Require Import TestSuite.admit.
-(* -*- coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
-(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines *)
-Set Universe Polymorphism.
-Record sigT' {A} (P : A -> Type) := existT' { projT1' : A; projT2' : P projT1' }.
-Notation "{ x : A &' P }" := (sigT' (A := A) (fun x => P)) : type_scope.
-Arguments existT' {A} P _ _.
-Axiom admit : forall {T}, T.
-Notation paths := identity .
-
-Unset Automatic Introduction.
-
-Definition UU := Set.
-
-Definition dirprod ( X Y : UU ) := sigT' ( fun x : X => Y ) .
-Definition dirprodpair { X Y : UU } := existT' ( fun x : X => Y ) .
-
-Definition ddualand { X Y P : UU } (xp : ( X -> P ) -> P ) ( yp : ( Y -> P ) -> P ) : ( dirprod X Y -> P ) -> P.
-Proof.
-  intros X Y P xp yp X0 .
-  set ( int1 := fun ypp : ( ( Y -> P ) -> P ) => fun x : X => yp ( fun y : Y => X0 ( dirprodpair x y) ) ) .
-  apply ( xp ( int1 yp ) ) .
-Defined .
-Definition weq ( X Y : UU )  : UU .
-intros; exact ( sigT' (fun f:X->Y => admit) ).
-Defined.
-Definition pr1weq ( X Y : UU):= @projT1' _ _ : weq X Y -> (X -> Y).
-Coercion pr1weq : weq >-> Funclass.
-
-Definition invweq { X Y : UU } ( w : weq X Y ) : weq Y X .
-admit.
-Defined.
-
-Definition hProp := sigT' (fun X : Type => admit).
-
-Definition hProppair ( X : UU ) ( is : admit ) : hProp@{i j Set k}.
-intros; exact (existT' (fun X : UU => admit ) X is ).
-Defined.
-Definition hProptoType := @projT1' _ _ : hProp -> Type .
-Coercion hProptoType: hProp >-> Sortclass.
-
-Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).
-
-Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit.
-
-Definition hinhfun { X Y : UU } ( f : X -> Y ) : ishinh_UU X -> ishinh_UU Y.
-intros X Y f; exact ( fun isx : ishinh X => fun P : _ =>  fun yp : Y -> P => isx P ( fun x : X => yp ( f x ) ) ).
-Defined.
-
-Definition hinhuniv { X : UU } { P : hProp } ( f : X -> P ) ( wit : ishinh_UU X ) : P.
-intros; exact (  wit P f ).
-Defined.
-
-Definition hinhand { X Y : UU } ( inx1 : ishinh_UU X ) ( iny1 : ishinh_UU Y) : ishinh ( dirprod X Y ).
-intros; exact ( fun P:_  => ddualand (inx1 P) (iny1 P)) .
-Defined.
-
-Definition UU' := Type.
-Definition hSet:= sigT' (fun X : UU' => admit) .
-Definition hSetpair := existT' (fun X : UU' => admit).
-Definition pr1hSet:= @projT1' UU (fun X : UU' => admit) : hSet -> Type.
-Coercion pr1hSet: hSet >-> Sortclass.
-
-Definition hPropset : hSet := existT' _ hProp admit .
-
-Definition hsubtypes ( X : UU ) : Type.
-intros; exact (X -> hProp ).
-Defined.
-Definition carrier { X : UU } ( A : hsubtypes X ) : Type.
-intros; exact (sigT' A).
-Defined.
-Coercion carrier : hsubtypes >-> Sortclass.
-
-Definition subtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : hsubtypes ( dirprod X Y ).
-admit.
-Defined.
-
-Lemma weqsubtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : weq ( subtypesdirprod A B ) ( dirprod A B ) .
-  admit.
-Defined.
-
-Lemma ishinhsubtypesdirprod  { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) ( isa : ishinh A ) ( isb : ishinh B ) : ishinh ( subtypesdirprod A B ) .
-Proof .
-  intros .
-  apply ( hinhfun ( invweq ( weqsubtypesdirprod A B ) ) ) .
-  apply hinhand .
-  apply isa .
-  apply isb .
-Defined .
-
-Definition hrel ( X : UU ) : Type.
-intros; exact ( X -> X -> hProp).
-Defined.
-
-Definition iseqrel { X : UU } ( R : hrel X ) : Type.
-admit.
-Defined.
-
-Definition eqrel ( X : UU ) : Type.
-intros; exact ( sigT' ( fun R : hrel X => iseqrel R ) ).
-Defined.
-Definition pr1eqrel ( X : UU ) : eqrel X -> ( X -> ( X -> hProp ) ) := @projT1' _ _ .
-Coercion pr1eqrel : eqrel >-> Funclass .
-
-Definition hreldirprod { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) : hrel ( dirprod X Y ) .
-admit.
-Defined.
-Set Printing Universes.
-Print hProp.
-Print ishinh_UU.
-Print hProppair.
-Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type.
-intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) )) .
-Defined.
-Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
-intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact ax2.
-Defined.
-
-Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X }  : iseqclass R A -> ishinh ( carrier A ) .
-intros X R A. exact (fun is : iseqclass R A => projT1' _ is ).
-Defined.
-
-Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) .
-Proof .
-  intros .
-  set ( XY := dirprod X Y ) .
-  set ( AB := subtypesdirprod A B ) .
-  set ( RQ := hreldirprod R Q ) .
-  set ( ax0 := ishinhsubtypesdirprod  A B ( eqax0 isa ) admit ) .
-  apply ( iseqclassconstr _ ax0 admit admit ) .
-Defined .
-
-Definition image { X Y : UU } ( f : X -> Y ) : Type.
-intros; exact ( sigT' ( fun y : Y => admit ) ).
-Defined.
-Definition pr1image { X Y : UU } ( f : X -> Y ) : image f -> Y.
-intros X Y f; exact ( @projT1' _  ( fun y : Y => admit ) ).
-Defined.
-
-Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f.
-  admit.
-Defined.
-
-Definition setquot { X : UU } ( R : hrel X ) : Set.
-intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ).
-Defined.
-Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R.
-intros; exact (existT' _ A is ).
-Defined.
-Definition pr1setquot { X : UU } ( R : hrel X ) : setquot R -> ( hsubtypes X ).
-intros X R.
-exact ( @projT1' _ ( fun A : _ => iseqclass R A ) ).
-Defined.
-Coercion pr1setquot : setquot >-> hsubtypes .
-
-Definition setquotinset { X : UU } ( R : hrel X ) : hSet.
-intros; exact ( hSetpair (setquot R) admit) .
-Defined.
-
-Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
-intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _  ( projT2' _ cd ) ) ) ).
-Defined.
-
-Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) := forall x x' x0 x0' : X , R x x' ->  R x0 x0' ->  paths ( f x x0 ) ( f x' x0' ) .
-
-Definition binop ( X : UU ) : Type.
-intros; exact ( X -> X -> X ).
-Defined.
-
-Definition setwithbinop : Type.
-exact (sigT' ( fun X : hSet => binop X ) ).
-Defined.
-Definition pr1setwithbinop : setwithbinop -> hSet@{j k Set l}.
-unfold setwithbinop.
-exact ( @projT1' _ ( fun X : hSet@{j k Set l} => binop@{Set} X ) ).
-Defined.
-Coercion pr1setwithbinop : setwithbinop >-> hSet .
-
-Definition op { X : setwithbinop } : binop X.
-intros; exact ( projT2' _ X ).
-Defined.
-
-Definition subsetswithbinop { X : setwithbinop } : Type.
-admit.
-Defined.
-
-Definition carrierofasubsetwithbinop { X : setwithbinop } ( A : @subsetswithbinop X ) : setwithbinop .
-admit.
-Defined.
-
-Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop .
-
-Definition binopeqrel { X : setwithbinop } : Type.
-intros; exact (sigT' ( fun R : eqrel X => admit ) ).
-Defined.
-Definition binopeqrelpair { X : setwithbinop } := existT' ( fun R : eqrel X => admit ).
-Definition pr1binopeqrel ( X : setwithbinop ) : @binopeqrel X -> eqrel X.
-intros X; exact ( @projT1' _ ( fun R : eqrel X => admit ) ) .
-Defined.
-Coercion pr1binopeqrel : binopeqrel >-> eqrel .
-
-Definition setwithbinopdirprod ( X Y : setwithbinop ) : setwithbinop .
-admit.
-Defined.
-
-Definition monoid : Type.
-exact ( sigT' ( fun X : setwithbinop => admit ) ).
-Defined.
-Definition monoidpair := existT' ( fun X : setwithbinop => admit ) .
-Definition pr1monoid : monoid -> setwithbinop := @projT1' _ _ .
-Coercion pr1monoid : monoid >-> setwithbinop .
-
-Notation "x + y" := ( op x y ) : addmonoid_scope .
-
-Definition submonoids { X : monoid } : Type.
-admit.
-Defined.
-
-Definition submonoidstosubsetswithbinop ( X : monoid ) : @submonoids X -> @subsetswithbinop X.
-admit.
-Defined.
-Coercion  submonoidstosubsetswithbinop : submonoids >-> subsetswithbinop .
-
-Definition abmonoid : Type.
-exact (sigT' ( fun X : setwithbinop => admit ) ).
-Defined.
-
-Definition abmonoidtomonoid : abmonoid -> monoid.
-exact (fun X : _ => monoidpair ( projT1' _ X ) admit ).
-Defined.
-Coercion abmonoidtomonoid : abmonoid >-> monoid .
-
-Definition subabmonoids { X : abmonoid } := @submonoids X .
-
-Definition carrierofsubabmonoid { X : abmonoid } ( A : @subabmonoids X ) : abmonoid .
-Proof .
-  intros .
-  unfold subabmonoids in A .
-  split with A .
-  admit.
-Defined .
-
-Coercion carrierofsubabmonoid : subabmonoids >-> abmonoid .
-
-Definition abmonoiddirprod ( X Y : abmonoid ) : abmonoid .
-Proof .
-  intros .
-  split with ( setwithbinopdirprod X Y ) .
-  admit.
-Defined .
-
-Open Scope addmonoid_scope .
-
-Definition eqrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : eqrel ( setwithbinopdirprod X A ).
-admit.
-Defined.
-
-Definition binopeqrelabmonoidfrac ( X : abmonoid ) ( A : @subabmonoids X ) : @binopeqrel ( abmonoiddirprod X A ).
-intros; exact ( @binopeqrelpair ( setwithbinopdirprod X A ) ( eqrelabmonoidfrac X A ) admit ).
-Defined.
-
-Theorem setquotuniv  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ) : Y .
-Proof.
-  intros.
-  apply ( pr1image ( fun x : c => f ( projT1' _ x ) ) ) .
-  apply ( @hinhuniv ( projT1' _ c ) ( hProppair _ admit ) ( prtoimage ( fun x : c => f ( projT1' _ x ) ) ) ) .
-  pose ( eqax0 ( projT2' _ c ) )  as h.
-  simpl in *.
-  Set Printing Universes.
-  exact h.
-Defined .
-
-Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) : Y .
-Proof.
-  intros .
-  set ( RR := hreldirprod R R ) .
-  apply (setquotuniv RR Y admit).
-  apply dirprodtosetquot.
-  apply dirprodpair.
-  exact c.
-  exact c0.
-Defined .
-
-Definition  setquotfun2  { X Y : UU } ( RX : hrel X ) ( RY : eqrel Y ) ( f : X -> X -> Y ) ( cx cx0 : setquot RX ) : setquot RY .
-Proof .
-  intros .
-  apply ( setquotuniv2 RX ( setquotinset RY ) admit admit admit admit ) .
-Defined .
-
-Definition quotrel  { X : UU } { R : hrel X } : hrel ( setquot R ).
-intros; exact ( setquotuniv2 R hPropset admit admit ).
-Defined.
-
-Definition setwithbinopquot { X : setwithbinop } ( R : @binopeqrel X ) : setwithbinop .
-Proof .
-  intros .
-  split with ( setquotinset R )  .
-  set ( qtmlt := setquotfun2 R R op ) .
-  simpl .
-  unfold binop .
-  apply qtmlt .
-Defined .
-
-Definition abmonoidquot { X : abmonoid } ( R : @binopeqrel X ) : abmonoid .
-Proof .
-  intros .
-  split with  ( setwithbinopquot R )  .
-  admit.
-Defined .
-
-Definition abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : abmonoid.
-intros; exact ( @abmonoidquot (abmonoiddirprod X (@carrierofsubabmonoid X A)) ( binopeqrelabmonoidfrac X A ) ).
-Defined.
-
-Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setquot (setwithbinopdirprod X A) (eqrelabmonoidfrac X A)).
-intros; exact (@quotrel _ _).
-Defined.
-
-Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
-
-Definition ispartlbinopabmonoidfracrel_type : Type :=
-  forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), 
-    @abmonoidfracrel X A ( ( admit + z ) )admit.
-
-Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
-                                      ispartlbinopabmonoidfracrel_type in exact t)$.
-
-Unset Kernel Term Sharing.
-
-Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
-
-Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
-                                      ispartlbinopabmonoidfracrel_type in exact t)$.
-
-- 
cgit v1.2.3


From 6b9ff2261c738ff8ce47b75e5ced2b85476b6210 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:46:08 +0200
Subject: Univs: fix test-suite file for #4287, now properly rejected.

---
 test-suite/bugs/closed/4287.v | 52 ++-----------------------------------------
 1 file changed, 2 insertions(+), 50 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 732f19f33c..e139c5b6c9 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -100,35 +100,15 @@ End Hurkens.
 
 Polymorphic Record box (T : Type) := wrap {unwrap : T}.
 
-(* Here we instantiate to Prop *)
-(* Here we instantiate to Prop *)
+(* Here we instantiate to Set *)
 
-Fail Definition down (x : Type) : Set := box x.
-Definition down (x : Set) : Set := box x.
+Fail Definition down (x : Type) : Prop := box x.
 Definition up (x : Prop) : Type := x.
 
 Fail Definition back A : up (down A) -> A := unwrap A.
 
 Fail Definition forth A : A -> up (down A) := wrap A.
 
-(* Lemma backforth (A:Type) (P:A->Type) (a:A) : *)
-(*       P (back A (forth A a)) -> P a. *)
-(* Proof. *)
-(* intros; assumption. *)
-(* Qed. *)
-
-(* Lemma backforth_r (A:Type) (P:A->Type) (a:A) : *)
-(*       P a -> P (back A (forth A a)). *)
-(* Proof. *)
-(* intros; assumption. *)
-(* Qed. *)
-
-(* Theorem bad : False. *)
-(* apply (paradox down up back forth backforth backforth_r). *)
-(* Qed. *)
-
-(* Print Assumptions bad. *)
-
 Definition id {A : Type} (a : A) := a.
 Definition setlt (A : Type@{i}) :=
   let foo := Type@{i} : Type@{j} in True.
@@ -142,31 +122,3 @@ Check @setle@{Prop j}.
 
 Fail Definition foo := @setle@{j Prop}.
 Definition foo := @setle@{Prop j}.
-
-(* Definition up (x : Prop) : Type := x. *)
-
-(* Definition back A : up (down A) -> A := unwrap A. *)
-
-(* Definition forth A : A -> up (down A) := wrap A. *)
-
-(* Lemma backforth (A:Type) (P:A->Type) (a:A) : *)
-(*       P (back A (forth A a)) -> P a. *)
-(* Proof. *)
-(* intros; assumption. *)
-(* Qed. *)
-
-(* Lemma backforth_r (A:Type) (P:A->Type) (a:A) : *)
-(*       P a -> P (back A (forth A a)). *)
-(* Proof. *)
-(* intros; assumption. *)
-(* Qed. *)
-
-(* Theorem bad : False. *)
-(* apply (paradox down up back forth backforth backforth_r). *)
-(* Qed. *)
-
-(* Print Assumptions bad. *)
-
-(* Polymorphic Record box (T : Type) := wrap {unwrap : T}. *)
-
-(* Definition down (x : Type) : Prop := box x. *)
-- 
cgit v1.2.3