Merge branch 'v8.5'

18 files changed, 377 insertions, 346 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 39c36d541..31b212900 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -388,7 +388,7 @@ misc/deps-order.log:
 	} > "$@"
 
 # Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 3
+EXPECTED_UNIVERSES := 5
 universes: misc/universes.log
 misc/universes.log: misc/universes/all_stdlib.v
 	@echo "TEST      misc/universes"
diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
new file mode 100644
index 000000000..13ec5bea9
--- /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
diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
new file mode 100644
index 000000000..a5f4ae64a
--- /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
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
deleted file mode 100644
index 980431576..000000000
--- 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 ) : Type.
-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 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)$.
-
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index e63c46da0..fb3791af5 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.
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/closed/3685.v
index b2b5db6be..a5bea34a9 100644
--- a/test-suite/bugs/opened/3685.v
+++ b/test-suite/bugs/closed/3685.v
@@ -63,7 +63,7 @@ Module Success.
 End Success.
 Module Bad.
   Include PointwiseCore.
-  Fail Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
+  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
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
new file mode 100644
index 000000000..b9b2dd6b3
--- /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 -> _).
diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v
new file mode 100644
index 000000000..66343d667
--- /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
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
new file mode 100644
index 000000000..e139c5b6c
--- /dev/null
+++ b/test-suite/bugs/closed/4287.v
@@ -0,0 +1,124 @@
+
+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 Set *)
+
+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.
+
+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}.
diff --git a/test-suite/bugs/closed/4294.v b/test-suite/bugs/closed/4294.v
new file mode 100644
index 000000000..1d5e3c71b
--- /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 000000000..875612ddf
--- /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.
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
new file mode 100644
index 000000000..3b00efb21
--- /dev/null
+++ b/test-suite/bugs/closed/4301.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Parameter U : Type.
+End Foo.
+
+Module Lower (X : Foo with Definition U := True : Type).
+End Lower.
+
+Module M : Foo.
+  Definition U := nat : Type@{i}. 
+End M.
diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v
new file mode 100644
index 000000000..8e1bb3100
--- /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
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index a14fb6aa5..e2bf1dbed 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 38943ab35..f382dac97 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 4f5ef9974..b6c0da76b 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 }
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
index 05ee6c7b6..e46ea58bb 100644
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -116,7 +116,8 @@ Section fully_faithful_helpers.
   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).
+  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
@@ -126,7 +127,7 @@ Section fully_faithful_helpers.
           => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
   admit.
   Undo.
-  Fail set (isequiv_isepimorphism_ismonomorphism'
+  Fail set (isequiv_isepimorphism_ismonomorphism
        := fun `{Univalence}
               (Hepi : IsEpimorphism (m : morphism set_cat x y))
               (Hmono : IsMonomorphism (m : morphism set_cat x y))
diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v
index 64faa0ce0..eda4a1867 100644
--- a/test-suite/failure/guard-cofix.v
+++ b/test-suite/failure/guard-cofix.v
@@ -25,7 +25,7 @@ Fail Definition ff : False := match loop with CF _ t => t end.
 
 (* Second example *)
 
-Inductive omega := Omega : omega -> omega.
+Inductive omega : Prop := Omega : omega -> omega.
 
 Lemma H : omega = CoFalse.
 Proof.