Imported Upstream version 8.5~beta3+dfsg

84 files changed, 2509 insertions, 348 deletions

diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
new file mode 100644
index 00000000..13ec5bea
--- /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/2243.v b/test-suite/bugs/closed/2243.v
new file mode 100644
index 00000000..6d45c9a0
--- /dev/null
+++ b/test-suite/bugs/closed/2243.v
@@ -0,0 +1,9 @@
+Inductive is_nul: nat -> Prop := X: is_nul 0.
+Section O.
+Variable u: nat.
+Variable H: is_nul u.
+Goal True.
+Proof.
+destruct H.
+Undo.
+revert H; intro H; destruct H.
diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
new file mode 100644
index 00000000..a5f4ae64
--- /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/3267.v b/test-suite/bugs/closed/3267.v
index 5ce1ddf0..8175d66a 100644
--- a/test-suite/bugs/closed/3267.v
+++ b/test-suite/bugs/closed/3267.v
@@ -34,3 +34,14 @@ Module d.
     debug eauto.
   Defined.
 End d.
+
+(* An other variant which was still failing in 8.5 beta2 *)
+
+Parameter A B : Prop.
+Axiom a:B.
+
+Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end.
+Goal (B -> id A) -> A.
+intros.
+eauto using a.
+Abort.
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
deleted file mode 100644
index 98043157..00000000
--- 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 e63c46da..fb3791af 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/closed/3330.v b/test-suite/bugs/closed/3330.v
index 4cd7c39e..e6a50449 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index b57b0a0f..f8113e4c 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 (*
 I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo].  (I think this worked in HoTT/coq, too.)  Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A].  (The issue is tricker when IsHProp uses [A] elsewhere, as in:
diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v
index 0e236c21..b8bb8bce 100644
--- a/test-suite/bugs/closed/3386.v
+++ b/test-suite/bugs/closed/3386.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
index ae212caa..cb435e78 100644
--- a/test-suite/bugs/closed/3387.v
+++ b/test-suite/bugs/closed/3387.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
new file mode 100644
index 00000000..dce73e1a
--- /dev/null
+++ b/test-suite/bugs/closed/3446.v
@@ -0,0 +1,51 @@
+(* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
+Module First.
+Set Asymmetric Patterns.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B).
+Set Universe Polymorphism.
+
+
+Notation "x → y" := (x -> y)
+  (at level 99, y at level 200, right associativity): type_scope.
+Record sigT A (P : A -> Type) :=
+  { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} s.
+Arguments projT2 {A P} s.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Reserved Notation "x = y" (at level 70, no associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y).
+Notation " x = y " := (paths x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope.
+
+
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v.
+Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}).
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) :=
+  @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _).
+End First.
+
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+Arguments projT1 {_ _} _.
+Notation "( x ; y )" := (existT _ x y).
+Notation pr1 := projT1.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT P) (pq : {p : u.1 = v.1 &  p # u.2 = v.2}), u = v.
+Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100.
+Admitted.
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := 
+  path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3461.v b/test-suite/bugs/closed/3461.v
new file mode 100644
index 00000000..1b625e6a
--- /dev/null
+++ b/test-suite/bugs/closed/3461.v
@@ -0,0 +1,5 @@
+Lemma foo (b : bool) :
+  exists x : nat, x = x.
+Proof.
+eexists. 
+Fail eexact (eq_refl b).
diff --git a/test-suite/bugs/closed/3509.v b/test-suite/bugs/closed/3509.v
new file mode 100644
index 00000000..82266226
--- /dev/null
+++ b/test-suite/bugs/closed/3509.v
@@ -0,0 +1,6 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 : bar.
+Hint Rewrite a2 : bar.
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
new file mode 100644
index 00000000..4cbae335
--- /dev/null
+++ b/test-suite/bugs/closed/3510.v
@@ -0,0 +1,5 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 a2 : bar.
diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v
index c862965d..d258bb31 100644
--- a/test-suite/bugs/closed/3539.v
+++ b/test-suite/bugs/closed/3539.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-no-native-compiler") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *)
 (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0
    coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *)
@@ -63,4 +63,4 @@ x' : forall (_ : T1) (_ : T), T2
 m : T3 (x' fst1 x2) (x' fst0 x2)
 Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with
 "?25 ?27".
- *)
\ No newline at end of file
+ *)
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index 50645090..da12b686 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 8657 lines to
 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines,
 then from 51 lines to 37 lines, then from 43 lines to 30 lines *)
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index b2aa8c3c..e2d79769 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Notation idmap := (fun x => x).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
new file mode 100644
index 00000000..378db685
--- /dev/null
+++ b/test-suite/bugs/closed/3593.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+Set Printing All.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
+simpl; intros.
+  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
+  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
index a5b0e934..e69ec109 100644
--- a/test-suite/bugs/closed/3666.v
+++ b/test-suite/bugs/closed/3666.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
new file mode 100644
index 00000000..a5bea34a
--- /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/closed/3690.v b/test-suite/bugs/closed/3690.v
index 4069e380..df9f5f47 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v
new file mode 100644
index 00000000..637b77cc
--- /dev/null
+++ b/test-suite/bugs/closed/3736.v
@@ -0,0 +1,8 @@
+(* Check non-error failure in case of unsupported decidability scheme *)
+Local Set Decidable Equality Schemes.
+
+Inductive a := A with b := B.
+
+(* But fails with error if explicitly asked for the scheme *)
+
+Fail Scheme Equality for a.
diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v
new file mode 100644
index 00000000..4dfb3380
--- /dev/null
+++ b/test-suite/bugs/closed/3743.v
@@ -0,0 +1,11 @@
+(* File reduced by coq-bug-finder from original input, then from 967 lines to 469 lines, then from 459 lines to 35 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
+Require Export Coq.Setoids.Setoid.
+
+Fail Add Parametric Relation A
+: A (@eq A)
+    transitivity proved by transitivity
+      as refine_rel.
+(* Toplevel input, characters 20-118:
+Anomaly: index to an anonymous variable. Please report. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
new file mode 100644
index 00000000..e203528f
--- /dev/null
+++ b/test-suite/bugs/closed/3777.v
@@ -0,0 +1,17 @@
+Unset Strict Universe Declaration.
+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/3779.v b/test-suite/bugs/closed/3779.v
new file mode 100644
index 00000000..2b44e225
--- /dev/null
+++ b/test-suite/bugs/closed/3779.v
@@ -0,0 +1,12 @@
+Unset Strict Universe Declaration.
+Set Universe Polymorphism.
+Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
+Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
+Section foo.
+  Universes sm lg.
+  Context (O : UnitSubuniverse@{sm lg}).
+  Context {A : Type@{sm}}.
+  Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C).
+  Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+  Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+End foo.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
index 6e19ddf8..a5c84e68 100644
--- a/test-suite/bugs/closed/3808.v
+++ b/test-suite/bugs/closed/3808.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
   := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v
new file mode 100644
index 00000000..355d23a5
--- /dev/null
+++ b/test-suite/bugs/closed/3819.v
@@ -0,0 +1,9 @@
+Record Op := { t : Type ; op : t -> t }.
+
+Canonical Structure OpType : Op := Build_Op Type (fun X => X).
+
+Lemma test1 (X:Type) : eq (op OpType X)  X.
+Proof eq_refl.
+
+Definition test2 (A:Type) : eq (op _ A)  A.
+Proof eq_refl.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
index 8da4f736..30261ed2 100644
--- a/test-suite/bugs/closed/3821.v
+++ b/test-suite/bugs/closed/3821.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
 
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 93208489..5013bc6a 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Notation Type0 := Set.
@@ -43,7 +44,7 @@ Notation IsHProp := (IsTrunc -1).
 Monomorphic Axiom dummy_funext_type : Type0.
 Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Record TruncType (n : trunc_index) := BuildTruncType {
diff --git a/test-suite/bugs/closed/3948.v b/test-suite/bugs/closed/3948.v
new file mode 100644
index 00000000..56b1e3ff
--- /dev/null
+++ b/test-suite/bugs/closed/3948.v
@@ -0,0 +1,24 @@
+Module Type S.
+Parameter t : Type.
+End S.
+
+Module Bar(X : S).
+Definition elt := X.t.
+Axiom fold : elt.
+End Bar.
+
+Module Make (Z: S) := Bar(Z).
+
+Declare Module Y : S.
+
+Module Type Interface.
+Parameter constant : unit.
+End Interface.
+
+Module DepMap : Interface.
+Module Dom := Make(Y).
+Definition constant : unit :=
+  let _ := @Dom.fold in tt.
+End DepMap.
+
+Print Assumptions DepMap.constant.
diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v
new file mode 100644
index 00000000..c19a2d4a
--- /dev/null
+++ b/test-suite/bugs/closed/3956.v
@@ -0,0 +1,143 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *)
+Set Universe Polymorphism.
+Set Primitive Projections.
+Close Scope nat_scope.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {A B} _ _.
+Arguments fst {A B} _ / .
+Arguments snd {A B} _ / .
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Unset Strict Universe Declaration.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}.
+
+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.
+Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z
+  := match p, q with idpath, idpath => idpath end.
+
+Definition path_prod {A B : Type} (z z' : A * B)
+: (fst z = fst z') -> (snd z = snd z') -> (z = z').
+Proof.
+  destruct z, z'; simpl; intros [] []; reflexivity.
+Defined.  
+
+Module Type TypeM.
+  Parameter m : Type2.
+End TypeM.
+
+Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM.
+  Definition m := XM.m * YM.m.
+End ProdM.
+
+Module Type FunctionM (XM YM : TypeM).
+  Parameter m : XM.m -> YM.m.
+End FunctionM.
+
+Module IdmapM (XM : TypeM) <: FunctionM XM XM.
+  Definition m := (fun x => x) : XM.m -> XM.m.
+End IdmapM.
+
+Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM).
+  Parameter m : forall x, fM.m x = gM.m x.
+End HomotopyM.
+
+Module ComposeM (XM YM ZM : TypeM)
+       (gM : FunctionM YM ZM) (fM : FunctionM XM YM)
+       <: FunctionM XM ZM.
+  Definition m := (fun x => gM.m (fM.m x)).
+End ComposeM.
+
+Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (gM : FunctionM XM ZM).
+  Parameter m : XM.m -> YM.m.
+  Parameter m_beta : forall x, fM.m (m x) = gM.m x.
+End CorecM.
+
+Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (hM kM : FunctionM XM YM).
+  Module fhM := ComposeM XM YM ZM fM hM.
+  Module fkM := ComposeM XM YM ZM fM kM.
+  Declare Module mM (pM : HomotopyM XM ZM fhM fkM)
+    : HomotopyM XM YM hM kM.
+End CoindpathsM.
+
+Module Type Comodality (XM : TypeM).
+  Parameter m : Type2.
+  Module mM <: TypeM.
+    Definition m := m.
+  End mM.
+  Parameter from : m -> XM.m.
+  Module fromM <: FunctionM mM XM.
+    Definition m := from.
+  End fromM.
+  Declare Module corecM : CorecM mM XM fromM.
+  Declare Module coindpathsM : CoindpathsM mM XM fromM.
+End Comodality.
+
+Module Comodality_Theory (F : Comodality).
+
+  Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module f_o_from_M <: FunctionM FXM.mM YM.
+      Definition m := fun x => fM.m (FXM.from x).
+    End f_o_from_M.
+    Module mM := FYM.corecM FXM.mM f_o_from_M.
+    Definition m := mM.m.
+  End F_functor_M.
+
+  Module F_prod_cmp_M (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module PM := ProdM XM YM.
+    Module PFM := ProdM FXM FYM.
+    Module fstM <: FunctionM PM XM.
+      Definition m := @fst XM.m YM.m.
+    End fstM.
+    Module sndM <: FunctionM PM YM.
+      Definition m := @snd XM.m YM.m.
+    End sndM.
+    Module FPM := F PM.
+    Module FfstM := F_functor_M PM XM fstM FPM FXM.
+    Module FsndM := F_functor_M PM YM sndM FPM FYM.
+    Definition m : FPM.m -> PFM.m
+      := fun z => (FfstM.m z , FsndM.m z).
+  End F_prod_cmp_M.
+
+  Module isequiv_F_prod_cmp_M
+         (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    (** The comparison map *)
+    Module cmpM := F_prod_cmp_M XM YM FXM FYM.
+    Module FPM := cmpM.FPM.
+    (** We construct an inverse to it using corecursion. *)
+    Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM.
+      Definition m : cmpM.PFM.m -> cmpM.PM.m
+        := fun z => ( FXM.from (fst z) , FYM.from (snd z) ).
+    End prod_from_M.
+    Module cmpinvM <: FunctionM cmpM.PFM FPM
+      := FPM.corecM cmpM.PFM prod_from_M.
+    (** We prove the first homotopy *)
+    Module cmpinv_o_cmp_M <: FunctionM FPM FPM
+      := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM.
+    Module idmap_FPM <: FunctionM FPM FPM
+      := IdmapM FPM.
+    Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
+    Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
+      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+      Proof.
+        intros x.
+        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+        apply path_prod@{i i i}; simpl.
+        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
+        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+      Defined.
+    End cip_FPHM.
+  End isequiv_F_prod_cmp_M.
+
+End Comodality_Theory.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v
new file mode 100644
index 00000000..b6be1595
--- /dev/null
+++ b/test-suite/bugs/closed/3974.v
@@ -0,0 +1,7 @@
+Module Type S.
+End S.
+
+Module Type M (X : S).
+  Fail Module P (X : S).
+  (* Used to say: Anomaly: X already exists. Please report. *)
+  (* Should rather say now: Error: X already exists. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v
new file mode 100644
index 00000000..95851c81
--- /dev/null
+++ b/test-suite/bugs/closed/3975.v
@@ -0,0 +1,8 @@
+Module Type S. End S.
+
+Module M (X:S). End M.
+
+Module Type P (X : S).
+  Print M.
+  (* Used to say: Anomaly: X already exists. Please report. *)
+  (* Should rather : print something :-) *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4034.v b/test-suite/bugs/closed/4034.v
new file mode 100644
index 00000000..3f7be4d1
--- /dev/null
+++ b/test-suite/bugs/closed/4034.v
@@ -0,0 +1,25 @@
+(* This checks compatibility of interpretation scope used for exact
+   between 8.4 and 8.5. See discussion at
+   https://coq.inria.fr/bugs/show_bug.cgi?id=4034. It is not clear
+   what we would like exactly, but certainly, if exact is interpreted
+   in a special scope, it should be interpreted consistently so also
+   in ltac code. *)
+
+Record Foo := {}.
+Bind Scope foo_scope with Foo.
+Notation "!" := Build_Foo : foo_scope.
+Notation "!" := 1 : core_scope.
+Open Scope foo_scope.
+Open Scope core_scope.
+
+Goal Foo.
+  Fail exact !.
+(* ... but maybe will we want it to succeed eventually if we ever
+   would be able to make it working the same in
+
+Ltac myexact e := exact e.
+
+Goal Foo.
+  myexact !.
+Defined.
+*)
diff --git a/test-suite/bugs/closed/4057.v b/test-suite/bugs/closed/4057.v
new file mode 100644
index 00000000..4f0e696c
--- /dev/null
+++ b/test-suite/bugs/closed/4057.v
@@ -0,0 +1,210 @@
+Require Coq.Strings.String.
+
+Set Implicit Arguments.
+
+Axiom falso : False.
+Ltac admit := destruct falso.
+
+Reserved Notation "[ x ]".
+
+Record string_like (CharType : Type) :=
+  {
+    String :> Type;
+    Singleton : CharType -> String where "[ x ]" := (Singleton x);
+    Empty : String;
+    Concat : String -> String -> String where "x ++ y" := (Concat x y);
+    bool_eq : String -> String -> bool;
+    bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+    Length : String -> nat
+  }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Infix "++" := (@Concat _ _) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+  := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Module Export ContextFreeGrammar.
+  Import Coq.Strings.String.
+  Import Coq.Lists.List.
+
+  Section cfg.
+    Variable CharType : Type.
+
+    Section definitions.
+
+      Inductive item :=
+    | NonTerminal (name : string).
+
+      Definition production := list item.
+      Definition productions := list production.
+
+      Record grammar :=
+        {
+          Start_symbol :> string;
+          Lookup :> string -> productions
+        }.
+    End definitions.
+
+    Section parse.
+      Variable String : string_like CharType.
+      Variable G : grammar.
+
+      Inductive parse_of : String -> productions -> Type :=
+      | ParseHead : forall str pat pats, parse_of_production str pat
+                                         -> parse_of str (pat::pats)
+      | ParseTail : forall str pat pats, parse_of str pats
+                                         -> parse_of str (pat::pats)
+      with parse_of_production : String -> production -> Type :=
+      | ParseProductionCons : forall str pat strs pats,
+                                parse_of_item str pat
+                                -> parse_of_production strs pats
+                                -> parse_of_production (str ++ strs) (pat::pats)
+      with parse_of_item : String -> item -> Type :=
+      | ParseNonTerminal : forall name str, parse_of str (Lookup G name)
+                                            -> parse_of_item str (NonTerminal 
+name).
+    End parse.
+  End cfg.
+
+End ContextFreeGrammar.
+Module Export ContextFreeGrammarProperties.
+
+  Section cfg.
+    Context CharType (String : string_like CharType) (G : grammar)
+            (P : String.string -> Type).
+
+    Fixpoint Forall_parse_of {str pats} (p : parse_of String G str pats)
+      := match p with
+           | @ParseHead _ _ _ str pat pats p'
+             => Forall_parse_of_production p'
+           | @ParseTail _ _ _ _ _ _ p'
+             => Forall_parse_of p'
+         end
+    with Forall_parse_of_production {str pat} (p : parse_of_production String G 
+str pat)
+         := let Forall_parse_of_item {str it} (p : parse_of_item String G str 
+it)
+                := match p return Type with
+                     | @ParseNonTerminal _ _ _ name str p'
+                       => (P name * Forall_parse_of p')%type
+                   end in
+            match p return Type with
+              | @ParseProductionCons _ _ _ str pat strs pats p' p''
+                => (Forall_parse_of_item p' * Forall_parse_of_production 
+p'')%type
+            end.
+
+    Definition Forall_parse_of_item {str it} (p : parse_of_item String G str it)
+      := match p return Type with
+           | @ParseNonTerminal _ _ _ name str p'
+             => (P name * Forall_parse_of p')%type
+         end.
+  End cfg.
+
+End ContextFreeGrammarProperties.
+
+Module Export DependentlyTyped.
+  Import Coq.Strings.String.
+
+  Section recursive_descent_parser.
+
+    Class parser_computational_predataT :=
+      { nonterminal_names_listT : Type;
+        initial_nonterminal_names_data : nonterminal_names_listT;
+        is_valid_nonterminal_name : nonterminal_names_listT -> string -> bool;
+        remove_nonterminal_name : nonterminal_names_listT -> string -> 
+nonterminal_names_listT }.
+
+  End recursive_descent_parser.
+
+End DependentlyTyped.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+
+Section cfg.
+  Context CharType (String : string_like CharType) (G : grammar).
+  Context (names_listT : Type)
+          (initial_names_data : names_listT)
+          (is_valid_name : names_listT -> string -> bool)
+          (remove_name : names_listT -> string -> names_listT).
+
+  Inductive minimal_parse_of
+  : forall (str0 : String) (valid : names_listT)
+           (str : String),
+      productions -> Type :=
+  | MinParseHead : forall str0 valid str pat pats,
+                     @minimal_parse_of_production str0 valid str pat
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  | MinParseTail : forall str0 valid str pat pats,
+                     @minimal_parse_of str0 valid str pats
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  with minimal_parse_of_production
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           production -> Type :=
+  | MinParseProductionNil : forall str0 valid,
+                              @minimal_parse_of_production str0 valid (Empty _) 
+nil
+  | MinParseProductionCons : forall str0 valid str strs pat pats,
+                               str ++ strs ≤s str0
+                               -> @minimal_parse_of_item str0 valid str pat
+                               -> @minimal_parse_of_production str0 valid strs 
+pats
+                               -> @minimal_parse_of_production str0 valid (str 
+++ strs) (pat::pats)
+  with minimal_parse_of_item
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           item -> Type :=
+  | MinParseNonTerminal
+    : forall str0 valid str name,
+        @minimal_parse_of_name str0 valid str name
+        -> @minimal_parse_of_item str0 valid str (NonTerminal name)
+  with minimal_parse_of_name
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall str0 valid name str,
+        @minimal_parse_of str initial_names_data str (Lookup G name)
+        -> @minimal_parse_of_name str0 valid str name
+  | MinParseNonTerminalStrEq
+    : forall str valid name,
+        @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+        -> @minimal_parse_of_name str valid str name.
+  Definition parse_of_item_name__of__minimal_parse_of_name
+  : forall {str0 valid str name} (p : @minimal_parse_of_name str0 valid str 
+name),
+      parse_of_item String G str (NonTerminal name).
+  Proof.
+    admit.
+  Defined.
+
+End cfg.
+
+Section recursive_descent_parser.
+  Context (CharType : Type)
+          (String : string_like CharType)
+          (G : grammar).
+  Context {premethods : parser_computational_predataT}.
+  Let P : string -> Prop.
+  Proof.
+    admit.
+  Defined.
+
+  Let mp_parse_nonterminal_name str0 valid str nonterminal_name
+    := { p' : minimal_parse_of_name String G initial_nonterminal_names_data 
+remove_nonterminal_name str0 valid str nonterminal_name & Forall_parse_of_item 
+P (parse_of_item_name__of__minimal_parse_of_name p') }.
+
+  Goal False.
+  Proof.
+    clear -mp_parse_nonterminal_name.
+    subst P.
+    simpl in *.
+    admit.
+  Qed.
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
new file mode 100644
index 00000000..21b03ce5
--- /dev/null
+++ b/test-suite/bugs/closed/4069.v
@@ -0,0 +1,51 @@
+
+Lemma test1 : 
+forall (v : nat) (f g : nat -> nat),
+f v = g v.
+intros. f_equal.
+(* 
+Goal in v8.5: f v = g v
+Goal in v8.4: v = v -> f v = g v
+Expected: f = g
+*)
+Admitted.
+
+Lemma test2 : 
+forall (v u : nat) (f g : nat -> nat),
+f v = g u.
+intros. f_equal.
+(* 
+In both v8.4 And v8.5
+Goal 1: v = u -> f v = g u
+Goal 2: v = u
+
+Expected Goal 1: f = g
+Expected Goal 2: v = u
+*)
+Admitted.
+
+Lemma test3 : 
+forall (v : nat) (u : list nat) (f : nat -> nat) (g : list nat -> nat),
+f v = g u.
+intros. f_equal.
+(* 
+In both v8.4 And v8.5, the goal is unchanged.
+*)
+Admitted.
+
+Require Import List.
+Lemma foo n (l k : list nat) : k ++ skipn n l = skipn n l.
+Proof. f_equal.
+(*
+  8.4: leaves the goal unchanged, i.e. k ++ skipn n l = skipn n l
+  8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l
+    and skipn n l = l
+*)
+Require Import List.
+Fixpoint replicate {A} (n : nat) (x : A) : list A :=
+  match n with 0 => nil | S n => x :: replicate n x end.
+Lemma bar {A} n m (x : A) : 
+  skipn n (replicate m x) = replicate (m - n) x ->
+  skipn n (replicate m x) = replicate (m - n) x.
+Proof. intros. f_equal.
+(* 8.5: one goal, n = m - n *)
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index 1449f242..e4d76732 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
@@ -163,7 +164,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
 
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Ltac done :=
diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
new file mode 100644
index 00000000..f808cb45
--- /dev/null
+++ b/test-suite/bugs/closed/4116.v
@@ -0,0 +1,383 @@
+(* File reduced by coq-bug-finder from original input, then from 13191 lines to 1315 lines, then from 1601 lines to 595 lines, then from 585 lines to 379 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 3 2015 3:50:31 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ac62cda8a4f488b94033b108c37556877232137a) *)
+
+Axiom admit : False.
+Ltac admit := exfalso; exact admit.
+
+Global Set Primitive Projections.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Reflexive {A} (R : relation A) :=
+  reflexivity : forall x : A, R x x.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Global Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: f == g
+  := fun x => match h with idpath => 1 end.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+                                               equiv_inv : B -> A ;
+                                               eisretr : Sect equiv_inv f;
+                                               eissect : Sect f equiv_inv;
+                                               eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+                                             }.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+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.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Local Open Scope trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+Notation "0" := (-1.+1) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
+  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  [
+      | (
+        let H := match goal with H := _ |- _ => constr:(H) end in
+        rename H into name) ].
+
+Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
+: transport P p u = transport idmap (ap P p) u
+  := match p with idpath => idpath end.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+
+  Let issect' := fun x =>
+                   ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+    admit.
+  Defined.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+
+End Adjointify.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+                                          trunctype_type : Type ;
+                                          istrunc_trunctype_type : IsTrunc n trunctype_type
+                                        }.
+Arguments trunctype_type {_} _.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hSet := 0-Type.
+
+Module Export Category.
+  Module Export Core.
+    Set Implicit Arguments.
+
+    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;
+
+          identity : forall x, morphism x x;
+          compose : forall s d d',
+                      morphism d d'
+                      -> morphism s d
+                      -> morphism s d'
+          where "f 'o' g" := (compose f g);
+
+          associativity : forall x1 x2 x3 x4
+                                 (m1 : morphism x1 x2)
+                                 (m2 : morphism x2 x3)
+                                 (m3 : morphism x3 x4),
+                            (m3 o m2) o m1 = m3 o (m2 o m1);
+
+          associativity_sym : forall x1 x2 x3 x4
+                                     (m1 : morphism x1 x2)
+                                     (m2 : morphism x2 x3)
+                                     (m3 : morphism x3 x4),
+                                m3 o (m2 o m1) = (m3 o m2) o m1;
+
+          left_identity : forall a b (f : morphism a b), identity b o f = f;
+          right_identity : forall a b (f : morphism a b), f o identity a = f;
+
+          identity_identity : forall x, identity x o identity x = identity x
+        }.
+    Arguments identity {!C%category} / x%object : rename.
+    Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
+
+    Definition Build_PreCategory
+               object morphism compose identity
+               associativity left_identity right_identity
+      := @Build_PreCategory'
+           object
+           morphism
+           compose
+           identity
+           associativity
+           (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _))
+           left_identity
+           right_identity
+           (fun _ => left_identity _ _ _).
+
+    Module Export CategoryCoreNotations.
+      Infix "o" := compose : morphism_scope.
+      Notation "1" := (identity _) : morphism_scope.
+    End CategoryCoreNotations.
+
+  End Core.
+
+End Category.
+Module Export Core.
+  Set Implicit Arguments.
+
+  Delimit Scope functor_scope with functor.
+
+  Local Open Scope morphism_scope.
+
+  Section Functor.
+    Variables C D : PreCategory.
+
+    Record Functor :=
+      {
+        object_of :> C -> D;
+        morphism_of : forall s d, morphism C s d
+                                  -> morphism D (object_of s) (object_of d);
+        composition_of : forall s d d'
+                                (m1 : morphism C s d) (m2: morphism C d d'),
+                           morphism_of _ _ (m2 o m1)
+                           = (morphism_of _ _ m2) o (morphism_of _ _ m1);
+        identity_of : forall x, morphism_of _ _ (identity x)
+                                = identity (object_of x)
+      }.
+  End Functor.
+  Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+End Core.
+Module Export Morphisms.
+  Set Implicit Arguments.
+
+  Local Open Scope category_scope.
+  Local Open Scope morphism_scope.
+
+  Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+    {
+      morphism_inverse : morphism C d s;
+      left_inverse : morphism_inverse o m = identity _;
+      right_inverse : m o morphism_inverse = identity _
+    }.
+
+  Class Isomorphic {C : PreCategory} s d :=
+    {
+      morphism_isomorphic :> morphism C s d;
+      isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+    }.
+
+  Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+  Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+
+  Section iso_equiv_relation.
+    Variable C : PreCategory.
+
+    Global Instance isisomorphism_identity (x : C) : IsIsomorphism (identity x)
+      := {| morphism_inverse := identity x;
+            left_inverse := left_identity C x x (identity x);
+            right_inverse := right_identity C x x (identity x) |}.
+
+    Global Instance isomorphic_refl : Reflexive (@Isomorphic C)
+      := fun x : C => {| morphism_isomorphic := identity x |}.
+
+    Definition idtoiso (x y : C) (H : x = y) : Isomorphic x y
+      := match H in (_ = y0) return (x <~=~> y0) with
+           | 1%path => reflexivity x
+         end.
+  End iso_equiv_relation.
+
+End Morphisms.
+
+Notation IsCategory C := (forall s d : object C, IsEquiv (@idtoiso C s d)).
+
+Notation isotoid C s d := (@equiv_inv _ _ (@idtoiso C s d) _).
+
+Notation cat_of obj :=
+  (@Build_PreCategory obj
+                      (fun x y => x -> y)
+                      (fun _ x => x)
+                      (fun _ _ _ f g => f o g)%core
+                      (fun _ _ _ _ _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+  ).
+Definition set_cat : PreCategory := cat_of hSet.
+Set Implicit Arguments.
+
+Local Open Scope morphism_scope.
+
+Section Grothendieck.
+  Variable C : PreCategory.
+  Variable F : Functor C set_cat.
+
+  Record Pair :=
+    {
+      c : C;
+      x : F c
+    }.
+
+  Local Notation Gmorphism s d :=
+    { f : morphism C s.(c) d.(c)
+    | morphism_of F f s.(x) = d.(x) }.
+
+  Definition identity_H s
+    := apD10 (identity_of F s.(c)) s.(x).
+
+  Definition Gidentity s : Gmorphism s s.
+  Proof.
+    exists 1.
+    apply identity_H.
+  Defined.
+
+  Definition Gcategory : PreCategory.
+  Proof.
+    refine (@Build_PreCategory
+              Pair
+              (fun s d => Gmorphism s d)
+              Gidentity
+              _
+              _
+              _
+              _); admit.
+  Defined.
+End Grothendieck.
+
+Lemma isotoid_1 {C} `{IsCategory C} {x : C} {H : IsIsomorphism (identity x)}
+: isotoid C x x {| morphism_isomorphic := (identity x) ; isisomorphism_isomorphic := H |}
+  = idpath.
+  admit.
+Defined.
+Generalizable All Variables.
+
+Section Grothendieck2.
+  Context `{IsCategory C}.
+  Variable F : Functor C set_cat.
+
+  Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
+  Proof.
+    intros s d.
+    refine (isequiv_adjointify _ _ _ _).
+    {
+      intro m.
+      transparent assert (H' : (s.(c) = d.(c))).
+      {
+        apply (idtoiso C (x := s.(c)) (y := d.(c)))^-1%function.
+        exists (m : morphism _ _ _).1.
+        admit.
+
+      }
+      {
+        transitivity {| x := transport (fun x => F x) H' s.(x) |}.
+        admit.
+
+        {
+          change d with {| c := d.(c) ; x := d.(x) |}; simpl.
+          apply ap.
+          subst H'.
+          simpl.
+          refine (transport_idmap_ap _ (fun x => F x : Type) _ _ _ _ @ _ @ (m : morphism _ _ _).2).
+          change (fun x => F x : Type) with (trunctype_type o object_of F)%function.
+          admit.
+        }
+      }
+    }
+    {
+      admit.
+    }
+
+    {
+      intro x.
+      hnf in s, d.
+      destruct x.
+      simpl.
+      erewrite @isotoid_1.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index 5f8c411c..d34a2b8b 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v
new file mode 100644
index 00000000..fec64555
--- /dev/null
+++ b/test-suite/bugs/closed/4151.v
@@ -0,0 +1,403 @@
+Lemma foo (H : forall A, A) : forall A, A.
+  Show Universes.
+  eexact H.
+Qed.
+
+(* File reduced by coq-bug-finder from original input, then from 6390 lines to 397 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 17 2015 12:34:25 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (1b3759e78f227eb85a128c58b8ce8c11509dd8c3) *)
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Import Coq.Lists.SetoidList.
+Require Export Coq.Program.Program.
+
+Global Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+
+Fixpoint combine_sig_helper {T} {P : T -> Prop} (ls : list T) : (forall x, In x ls -> P x) -> list (sig P).
+  admit.
+Defined.
+
+Lemma Forall_forall1_transparent_helper_1 {A P} {x : A} {xs : list A} {l : list A}
+      (H : Forall P l) (H' : x::xs = l)
+: P x.
+  admit.
+Defined.
+Lemma Forall_forall1_transparent_helper_2 {A P} {x : A} {xs : list A} {l : list A}
+      (H : Forall P l) (H' : x::xs = l)
+: Forall P xs.
+  admit.
+Defined.
+
+Fixpoint Forall_forall1_transparent {A} (P : A -> Prop) (l : list A) {struct l}
+: Forall P l -> forall x, In x l -> P x
+  := match l as l return Forall P l -> forall x, In x l -> P x with
+       | nil => fun _ _ f => match f : False with end
+       | x::xs => fun H x' H' =>
+                    match H' with
+                      | or_introl H'' => eq_rect x
+                                                 P
+                                                 (Forall_forall1_transparent_helper_1 H eq_refl)
+                                                 _
+                                                 H''
+                      | or_intror H'' => @Forall_forall1_transparent A P xs (Forall_forall1_transparent_helper_2 H eq_refl) _ H''
+                    end
+     end.
+
+Definition combine_sig {T P ls} (H : List.Forall P ls) : list (@sig T P)
+  := combine_sig_helper ls (@Forall_forall1_transparent T P ls H).
+Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type
+  := match ls with
+       | nil => P nil
+       | x::xs => (P (x::xs) * Forall_tails P xs)%type
+     end.
+
+Record string_like (CharType : Type) :=
+  {
+    String :> Type;
+    Singleton : CharType -> String where "[ x ]" := (Singleton x);
+    Empty : String;
+    Concat : String -> String -> String where "x ++ y" := (Concat x y);
+    bool_eq : String -> String -> bool;
+    bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+    Length : String -> nat;
+    Associativity : forall x y z, (x ++ y) ++ z = x ++ (y ++ z);
+    LeftId : forall x, Empty ++ x = x;
+    RightId : forall x, x ++ Empty = x;
+    Singleton_Length : forall x, Length (Singleton x) = 1;
+    Length_correct : forall s1 s2, Length s1 + Length s2 = Length (s1 ++ s2);
+    Length_Empty : Length Empty = 0;
+    Empty_Length : forall s1, Length s1 = 0 -> s1 = Empty;
+    Not_Singleton_Empty : forall x, Singleton x <> Empty;
+    SplitAt : nat -> String -> String * String;
+    SplitAt_correct : forall n s, fst (SplitAt n s) ++ snd (SplitAt n s) = s;
+    SplitAt_concat_correct : forall s1 s2, SplitAt (Length s1) (s1 ++ s2) = (s1, s2);
+    SplitAtLength_correct : forall n s, Length (fst (SplitAt n s)) = min (Length s) n
+  }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Notation "[[ x ]]" := (@Singleton _ _ x) : string_like_scope.
+Infix "++" := (@Concat _ _) : string_like_scope.
+Infix "=s" := (@bool_eq _ _) (at level 70, right associativity) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+  := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Record StringWithSplitState {CharType} (String : string_like CharType) (split_stateT : String -> Type) :=
+  { string_val :> String;
+    state_val : split_stateT string_val }.
+
+Module Export ContextFreeGrammar.
+  Require Import Coq.Strings.String.
+
+  Section cfg.
+    Variable CharType : Type.
+
+    Section definitions.
+
+      Inductive item :=
+    | Terminal (_ : CharType)
+    | NonTerminal (_ : string).
+
+      Definition production := list item.
+      Definition productions := list production.
+
+      Record grammar :=
+        {
+          Start_symbol :> string;
+          Lookup :> string -> productions;
+          Start_productions :> productions := Lookup Start_symbol;
+          Valid_nonterminals : list string;
+          Valid_productions : list productions := map Lookup Valid_nonterminals
+        }.
+    End definitions.
+
+  End cfg.
+
+End ContextFreeGrammar.
+Module Export BaseTypes.
+  Import Coq.Strings.String.
+
+  Local Open Scope string_like_scope.
+
+  Inductive any_grammar CharType :=
+  | include_item (_ : item CharType)
+  | include_production (_ : production CharType)
+  | include_productions (_ : productions CharType)
+  | include_nonterminal (_ : string).
+  Global Coercion include_item : item >-> any_grammar.
+  Global Coercion include_production : production >-> any_grammar.
+
+  Section recursive_descent_parser.
+    Context {CharType : Type}
+            {String : string_like CharType}
+            {G : grammar CharType}.
+
+    Class parser_computational_predataT :=
+      { nonterminals_listT : Type;
+        initial_nonterminals_data : nonterminals_listT;
+        is_valid_nonterminal : nonterminals_listT -> string -> bool;
+        remove_nonterminal : nonterminals_listT -> string -> nonterminals_listT;
+        nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop;
+        remove_nonterminal_dec : forall ls nonterminal,
+                                   is_valid_nonterminal ls nonterminal = true
+                                   -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls;
+        ntl_wf : well_founded nonterminals_listT_R }.
+
+    Class parser_computational_types_dataT :=
+      { predata :> parser_computational_predataT;
+        split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }.
+
+    Class parser_computational_dataT' `{parser_computational_types_dataT} :=
+      { split_string_for_production
+        : forall (str0 : String) (valid : nonterminals_listT) (it : item CharType) (its : production CharType) (str : StringWithSplitState String (split_stateT str0 valid (it::its : production CharType))),
+            list (StringWithSplitState String (split_stateT str0 valid it)
+                  * StringWithSplitState String (split_stateT str0 valid its));
+        split_string_for_production_correct
+        : forall str0 valid it its str,
+            let P f := List.Forall f (@split_string_for_production str0 valid it its str) in
+            P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true) }.
+  End recursive_descent_parser.
+
+End BaseTypes.
+Import Coq.Strings.String.
+
+Section cfg.
+  Context CharType (String : string_like CharType) (G : grammar CharType).
+  Context (names_listT : Type)
+          (initial_names_data : names_listT)
+          (is_valid_name : names_listT -> string -> bool)
+          (remove_name : names_listT -> string -> names_listT)
+          (names_listT_R : names_listT -> names_listT -> Prop)
+          (remove_name_dec : forall ls name,
+                               is_valid_name ls name = true
+                               -> names_listT_R (remove_name ls name) ls)
+          (remove_name_1
+           : forall ls ps ps',
+               is_valid_name (remove_name ls ps) ps' = true
+               -> is_valid_name ls ps' = true)
+          (remove_name_2
+           : forall ls ps ps',
+               is_valid_name (remove_name ls ps) ps' = false
+               <-> is_valid_name ls ps' = false \/ ps = ps')
+          (ntl_wf : well_founded names_listT_R).
+
+  Inductive minimal_parse_of
+  : forall (str0 : String) (valid : names_listT)
+           (str : String),
+      productions CharType -> Type :=
+  | MinParseHead : forall str0 valid str pat pats,
+                     @minimal_parse_of_production str0 valid str pat
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  | MinParseTail : forall str0 valid str pat pats,
+                     @minimal_parse_of str0 valid str pats
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  with minimal_parse_of_production
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           production CharType -> Type :=
+  | MinParseProductionNil : forall str0 valid,
+                              @minimal_parse_of_production str0 valid (Empty _) nil
+  | MinParseProductionCons : forall str0 valid str strs pat pats,
+                               str ++ strs ≤s str0
+                               -> @minimal_parse_of_item str0 valid str pat
+                               -> @minimal_parse_of_production str0 valid strs pats
+                               -> @minimal_parse_of_production str0 valid (str ++ strs) (pat::pats)
+  with minimal_parse_of_item
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           item CharType -> Type :=
+  | MinParseTerminal : forall str0 valid x,
+                         @minimal_parse_of_item str0 valid [[ x ]]%string_like (Terminal x)
+  | MinParseNonTerminal
+    : forall str0 valid str name,
+        @minimal_parse_of_name str0 valid str name
+        -> @minimal_parse_of_item str0 valid str (NonTerminal CharType name)
+  with minimal_parse_of_name
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall str0 valid name str,
+        Length str < Length str0
+        -> is_valid_name initial_names_data name = true
+        -> @minimal_parse_of str initial_names_data str (Lookup G name)
+        -> @minimal_parse_of_name str0 valid str name
+  | MinParseNonTerminalStrEq
+    : forall str valid name,
+        is_valid_name initial_names_data name = true
+        -> is_valid_name valid name = true
+        -> @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+        -> @minimal_parse_of_name str valid str name.
+End cfg.
+
+Local Coercion is_true : bool >-> Sortclass.
+
+Local Open Scope string_like_scope.
+
+Section general.
+  Context {CharType} {String : string_like CharType} {G : grammar CharType}.
+
+  Class boolean_parser_dataT :=
+    { predata :> parser_computational_predataT;
+      split_stateT : String -> Type;
+      data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |};
+      split_string_for_production
+      : forall it its,
+          StringWithSplitState String split_stateT
+          -> list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT);
+      split_string_for_production_correct
+      : forall it its (str : StringWithSplitState String split_stateT),
+          let P f := List.Forall f (split_string_for_production it its str) in
+          P (fun s1s2 =>
+               (fst s1s2 ++ snd s1s2 =s str) = true);
+      premethods :> parser_computational_dataT'
+      := @Build_parser_computational_dataT'
+           _ String data'
+           (fun _ _ => split_string_for_production)
+           (fun _ _ => split_string_for_production_correct) }.
+
+  Definition split_list_completeT `{data : boolean_parser_dataT}
+             {str0 valid}
+             (str : StringWithSplitState String split_stateT) (pf : str ≤s str0)
+             (split_list : list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT))
+             (it : item CharType) (its : production CharType)
+    := ({ s1s2 : String * String
+                 & (fst s1s2 ++ snd s1s2 =s str)
+                   * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it)
+                   * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type)
+       -> ({ s1s2 : StringWithSplitState String split_stateT * StringWithSplitState String split_stateT
+                    & (In s1s2 split_list)
+                      * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it)
+                      * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type).
+End general.
+
+Section recursive_descent_parser.
+  Context {CharType}
+          {String : string_like CharType}
+          {G : grammar CharType}.
+  Context `{data : @boolean_parser_dataT _ String}.
+
+  Section bool.
+    Section parts.
+      Definition parse_item
+                 (str_matches_nonterminal : string -> bool)
+                 (str : StringWithSplitState String split_stateT)
+                 (it : item CharType)
+      : bool
+        := match it with
+             | Terminal ch => [[ ch ]] =s str
+             | NonTerminal nt => str_matches_nonterminal nt
+           end.
+
+      Section production.
+        Context {str0}
+                (parse_nonterminal
+                 : forall (str : StringWithSplitState String split_stateT),
+                     str ≤s str0
+                     -> string
+                     -> bool).
+
+        Fixpoint parse_production
+                 (str : StringWithSplitState String split_stateT)
+                 (pf : str ≤s str0)
+                 (prod : production CharType)
+        : bool.
+        Proof.
+          refine
+            match prod with
+              | nil =>
+
+                str =s Empty _
+              | it::its
+                => let parse_production' := fun str pf => parse_production str pf its in
+                   fold_right
+                     orb
+                     false
+                     (let mapF f := map f (combine_sig (split_string_for_production_correct it its str)) in
+                      mapF (fun s1s2p =>
+                              (parse_item
+                                 (parse_nonterminal (fst (proj1_sig s1s2p)) _)
+                                 (fst (proj1_sig s1s2p))
+                                 it)
+                                && parse_production' (snd (proj1_sig s1s2p)) _)%bool)
+            end;
+          revert pf; clear; intros; admit.
+        Defined.
+      End production.
+
+    End parts.
+  End bool.
+End recursive_descent_parser.
+
+Section sound.
+  Context CharType (String : string_like CharType) (G : grammar CharType).
+  Context `{data : @boolean_parser_dataT CharType String}.
+
+  Section production.
+    Context (str0 : String)
+            (parse_nonterminal : forall (str : StringWithSplitState String split_stateT),
+                                   str ≤s str0
+                                   -> string
+                                   -> bool).
+
+    Definition parse_nonterminal_completeT P
+      := forall valid (str : StringWithSplitState String split_stateT) pf nonterminal (H_sub : P str0 valid nonterminal),
+           minimal_parse_of_name _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal
+           -> @parse_nonterminal str pf nonterminal = true.
+
+    Lemma parse_production_complete
+          valid Pv
+          (parse_nonterminal_complete : parse_nonterminal_completeT Pv)
+          (Hinit : forall str (pf : str ≤s str0) nonterminal,
+                     minimal_parse_of_name String G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal
+                     -> Pv str0 valid nonterminal)
+          (str : StringWithSplitState String split_stateT) (pf : str ≤s str0)
+          (prod : production CharType)
+          (split_string_for_production_complete'
+           : forall str0 valid str pf,
+               Forall_tails
+                 (fun prod' =>
+                    match prod' return Type with
+                      | nil => True
+                      | it::its => split_list_completeT (G := G) (valid := valid) (str0 := str0) str pf (split_string_for_production it its str) it its
+                    end)
+                 prod)
+    : minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str prod
+      -> parse_production parse_nonterminal str pf prod = true.
+      admit.
+    Defined.
+  End production.
+  Context (str0 : String)
+          (parse_nonterminal : forall (str : StringWithSplitState String split_stateT),
+                                 str ≤s str0
+                                 -> string
+                                 -> bool).
+
+  Goal forall (a : production CharType),
+         (forall (str1 : String) (valid : nonterminals_listT)
+                 (str : StringWithSplitState String split_stateT)
+                 (pf : str ≤s str1),
+            Forall_tails
+              (fun prod' : list (item CharType) =>
+                 match prod' with
+                   | [] => True
+                   | it :: its =>
+                     split_list_completeT (G := G) (valid := valid) str pf
+                                          (split_string_for_production it its str) it its
+                 end) a) ->
+         forall (str : String) (pf : str ≤s str0) (st : split_stateT str),
+           parse_production parse_nonterminal
+                            {| string_val := str; state_val := st |} pf a = true.
+  Proof.
+    intros a X **.
+    eapply parse_production_complete.
+    Focus 3.
+    exact X.
+    Undo.
+    assumption.
+    Undo.
+    eassumption. (* no applicable tactic *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v
new file mode 100644
index 00000000..aa2b189b
--- /dev/null
+++ b/test-suite/bugs/closed/4161.v
@@ -0,0 +1,27 @@
+
+    (* Inductive t : Type -> Type := *)
+    (* | Just : forall (A : Type), t A -> t A. *)
+
+    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
+    (*   match x in t A return t (A + unit) with *)
+    (*   | Just T x => @test T x *)
+    (*   end. *)
+
+
+    Definition Type1 := Type.
+Definition Type2 := Type.
+Definition cast (x:Type2) := x:Type1.
+Axiom f: Type2 -> Prop.
+Definition A :=
+ let T := fun A:Type1 => _ in
+ fun A':Type2 =>
+ eq_refl : T A' = f A' :> Prop.
+(* Type2 <= Type1... f A -> Type1 <= Type2 *)
+
+Inductive t : Type -> Type :=
+    | Just : forall (A : Type), t A -> t A.
+
+Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
+  match x in t A with
+  | Just B x => @test B x
+  end.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4191.v b/test-suite/bugs/closed/4191.v
new file mode 100644
index 00000000..290bb384
--- /dev/null
+++ b/test-suite/bugs/closed/4191.v
@@ -0,0 +1,5 @@
+(* Test maximal implicit arguments in the presence of let-ins *)
+Definition foo (x := 1) {y : nat} (H : y = y) : True := I.
+Definition bar {y : nat} (x := 1) (H : y = y) : True := I.
+Check bar (eq_refl 1).
+Check foo (eq_refl 1). 
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
new file mode 100644
index 00000000..f85a6026
--- /dev/null
+++ b/test-suite/bugs/closed/4198.v
@@ -0,0 +1,37 @@
+(* Check that the subterms of the predicate of a match are taken into account *)
+
+Require Import List.
+Open Scope list_scope.
+Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
+       let k :=
+           (match H in (_ = y) return x = hd x y with
+              | eq_refl => eq_refl
+            end : x = x')
+       in k = k.
+  simpl.
+  intros.
+  match goal with
+    | [ |- appcontext G[@hd] ] => idtac
+  end.
+
+(* This second example comes from CFGV where inspecting subterms of a
+   match is expecting to inspect first the term to match (even though
+   it would certainly be better to provide a "match x with _ end"
+   construct for generically matching a "match") *)
+
+Ltac find_head_of_head_match T :=
+  match T with context [?E] => 
+    match T with  
+    | E => fail 1 
+    | _ => constr:(E) 
+    end 
+  end.
+
+Ltac mydestruct :=
+  match goal with 
+  | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E
+  end.
+
+Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
+intros.
+mydestruct.
diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v
new file mode 100644
index 00000000..076a3c3d
--- /dev/null
+++ b/test-suite/bugs/closed/4203.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record ops {T:Type} := { is_ok : T -> Prop; constant : T }.
+Arguments ops : clear implicits.
+
+Record ops_ok {T} (Ops:ops T) := { constant_ok : is_ok Ops (constant Ops) }.
+
+Definition nat_ops : ops nat := {| is_ok := fun n => n = 1; constant := 1 |}.
+Definition nat_ops_ok : ops_ok nat_ops.
+Proof.
+  split. cbn. apply eq_refl.
+Qed.
+
+Definition t := Eval lazy in constant_ok nat_ops nat_ops_ok.
+Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok.
+Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok.
+
+Check (eq_refl t : t = t').
+Check (eq_refl t : t = t'').
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v
new file mode 100644
index 00000000..c40dfcc1
--- /dev/null
+++ b/test-suite/bugs/closed/4205.v
@@ -0,0 +1,8 @@
+(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
+
+
+Inductive test : nat -> nat -> nat -> nat -> Prop :=
+  | test1 : forall m n, test m n m n.
+
+Goal test 1 2 3 4.
+erewrite f_equal2 with (f := fun k l => test _ _ k l).
diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v
new file mode 100644
index 00000000..ae7f7467
--- /dev/null
+++ b/test-suite/bugs/closed/4216.v
@@ -0,0 +1,20 @@
+Generalizable Variables T A.
+
+Inductive path `(a: A): A -> Type := idpath: path a a.
+
+Class TMonad (T: Type -> Type) := {
+  bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B;
+  ret: forall {A: Type}, A -> T A;
+  ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A),
+                 path (bind (ret a) k) (k a)
+  }.
+
+Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A)
+                  => bind t (fun a => bind f (fun g => ret (g a) )).
+Let T_pure `{TMonad T} := @ret _ _.
+
+Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): 
+        path (T_fzip A A (T_pure (A -> A) t) x) x.
+  unfold T_fzip, T_pure.
+  Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)).
+
diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v
new file mode 100644
index 00000000..19973f30
--- /dev/null
+++ b/test-suite/bugs/closed/4217.v
@@ -0,0 +1,6 @@
+(* Checking correct index of implicit by pos in fixpoints *)
+
+Fixpoint ith_default
+         {default_A : nat}
+         {As : list nat}
+         {struct As} : Set.
diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v
new file mode 100644
index 00000000..bc120fb1
--- /dev/null
+++ b/test-suite/bugs/closed/4221.v
@@ -0,0 +1,9 @@
+(* Some test checking that interpreting binder names using ltac
+   context does not accidentally break the bindings *)
+
+Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
+  intros H0 x.
+  lazymatch goal with
+    | [ x : forall k : nat, _ |- _ ]
+      => specialize (fun H0 => x 1 H0)
+  end.
diff --git a/test-suite/bugs/closed/4232.v b/test-suite/bugs/closed/4232.v
new file mode 100644
index 00000000..61e544a9
--- /dev/null
+++ b/test-suite/bugs/closed/4232.v
@@ -0,0 +1,20 @@
+Require Import Setoid Morphisms Vector.
+
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Global Declare Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n).
+Global Declare Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n).
+
+Global Declare Instance tl_proper1 {A} `{Equiv A} n:
+  Proper ((equiv) ==> (equiv))
+         (@tl A n).
+
+Lemma test:
+  forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)),
+    (equiv xa ya) -> equiv (tl xa) (tl ya).
+Proof.
+  intros A R HA n xa ya Heq.
+  setoid_rewrite Heq.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/4234.v b/test-suite/bugs/closed/4234.v
new file mode 100644
index 00000000..348dd49d
--- /dev/null
+++ b/test-suite/bugs/closed/4234.v
@@ -0,0 +1,7 @@
+Definition UU := Type.
+
+Definition dirprodpair {X Y : UU} := existT (fun x : X => Y).
+
+Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }.
+Proof.
+  refine (dirprodpair _ (fun x => _)).
diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v
new file mode 100644
index 00000000..083c59fe
--- /dev/null
+++ b/test-suite/bugs/closed/4240.v
@@ -0,0 +1,12 @@
+(* Check that closure of filter did not restrict the former evar filter *)
+
+Lemma foo (new : nat) : False.
+evar (H1: nat).
+set (H3 := 0).
+assert (H3' := id H3).
+evar (H5: nat).
+clear H3.
+assert (H5 = new).
+unfold H5.
+unfold H1.
+exact (eq_refl new).
diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v
new file mode 100644
index 00000000..66343d66
--- /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/4254.v b/test-suite/bugs/closed/4254.v
new file mode 100644
index 00000000..ef219973
--- /dev/null
+++ b/test-suite/bugs/closed/4254.v
@@ -0,0 +1,13 @@
+Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+
+Module WithPoly.
+Polymorphic Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+End WithPoly.
diff --git a/test-suite/bugs/closed/4272.v b/test-suite/bugs/closed/4272.v
new file mode 100644
index 00000000..aeb4c9bb
--- /dev/null
+++ b/test-suite/bugs/closed/4272.v
@@ -0,0 +1,12 @@
+Set Implicit Arguments.
+
+Record foo := Foo { p1 : Type; p2 : p1 }.
+
+Variable x : foo.
+
+Let p := match x with @Foo a b => a end.
+
+Notation "@ 'id'"  := 3 (at level 10).
+Notation "@ 'sval'" := 3 (at level 10).
+
+Let q := match x with @Foo a b => a end.
diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v
new file mode 100644
index 00000000..ba82e6c3
--- /dev/null
+++ b/test-suite/bugs/closed/4276.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+
+Record box (T U : Type) (x := T) := wrap { unwrap : T }.
+Definition mybox : box True False := wrap _ _ I.
+Definition unwrap' := @unwrap.
+
+Definition bad' : True := mybox.(unwrap _ _). 
+
+Fail Definition bad : False := unwrap _ _ mybox.
+
+(* Closed under the global context *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4280.v b/test-suite/bugs/closed/4280.v
new file mode 100644
index 00000000..fd789750
--- /dev/null
+++ b/test-suite/bugs/closed/4280.v
@@ -0,0 +1,24 @@
+Require Import ZArith.
+Require Import Eqdep_dec.
+Local Open Scope Z_scope.
+
+Definition t := { n: Z | n > 1 }.
+
+Program Definition two : t := 2.
+Next Obligation. omega. Qed.
+
+Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
+  if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
+Next Obligation.
+  destruct x as [x Px], y as [y Py]. simpl in H; subst y.
+  f_equal. apply UIP_dec. decide equality.
+Qed.
+Next Obligation.
+  congruence.
+Qed.
+
+Definition t_list_eq: forall (x y: list t), {x=y} + {x<>y}.
+Proof. decide equality. apply t_eq. Defined.
+
+Goal match t_list_eq (two::nil) (two::nil) with left _ => True | right _ => False end.
+Proof. exact I. Qed.
diff --git a/test-suite/bugs/closed/4283.v b/test-suite/bugs/closed/4283.v
new file mode 100644
index 00000000..e06998b7
--- /dev/null
+++ b/test-suite/bugs/closed/4283.v
@@ -0,0 +1,8 @@
+Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl.
+
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
new file mode 100644
index 00000000..0623cf5b
--- /dev/null
+++ b/test-suite/bugs/closed/4287.v
@@ -0,0 +1,125 @@
+Unset Strict Universe Declaration.
+
+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 00000000..1d5e3c71
--- /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 00000000..875612dd
--- /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/4299.v b/test-suite/bugs/closed/4299.v
new file mode 100644
index 00000000..955c3017
--- /dev/null
+++ b/test-suite/bugs/closed/4299.v
@@ -0,0 +1,12 @@
+Unset Strict Universe Declaration.
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type : Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type : Type.
+  Definition U := let X := Type in Type.
+  Definition eq : Type = U := eq_refl.
+Fail End M.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
new file mode 100644
index 00000000..b4e17c22
--- /dev/null
+++ b/test-suite/bugs/closed/4301.v
@@ -0,0 +1,13 @@
+Unset Strict Universe Declaration.
+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/4305.v b/test-suite/bugs/closed/4305.v
new file mode 100644
index 00000000..39fc02d2
--- /dev/null
+++ b/test-suite/bugs/closed/4305.v
@@ -0,0 +1,17 @@
+(* Check fallback when an abbreviation is not interpretable as a pattern *)
+
+Notation foo := Type.
+
+Definition t :=
+  match 0 with
+  | S foo => foo
+  | _ => 0
+  end.
+
+Notation bar := (option Type).
+
+Definition u :=
+  match 0 with
+  | S bar => bar
+  | _ => 0
+  end.
diff --git a/test-suite/bugs/closed/4316.v b/test-suite/bugs/closed/4316.v
new file mode 100644
index 00000000..68dec133
--- /dev/null
+++ b/test-suite/bugs/closed/4316.v
@@ -0,0 +1,3 @@
+Ltac tac := idtac.
+Reset tac.
+Ltac tac := idtac.
diff --git a/test-suite/bugs/closed/4318.v b/test-suite/bugs/closed/4318.v
new file mode 100644
index 00000000..e3140ed5
--- /dev/null
+++ b/test-suite/bugs/closed/4318.v
@@ -0,0 +1,2 @@
+(* Check no anomaly is raised *)
+Fail Definition foo p := match p with (x, y) z => tt end.
diff --git a/test-suite/bugs/closed/4325.v b/test-suite/bugs/closed/4325.v
new file mode 100644
index 00000000..af69ca04
--- /dev/null
+++ b/test-suite/bugs/closed/4325.v
@@ -0,0 +1,5 @@
+Goal (forall a b : nat, Set = (a = b)) -> Set.
+Proof.
+  clear.
+  intro H.
+  erewrite (fun H' => H _ H').
diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v
new file mode 100644
index 00000000..8e1bb310
--- /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/4346.v b/test-suite/bugs/closed/4346.v
new file mode 100644
index 00000000..b50dff24
--- /dev/null
+++ b/test-suite/bugs/closed/4346.v
@@ -0,0 +1,2 @@
+Check (Set <: Type).
+Check (Set <<: Type).
diff --git a/test-suite/bugs/closed/4347.v b/test-suite/bugs/closed/4347.v
new file mode 100644
index 00000000..29686a26
--- /dev/null
+++ b/test-suite/bugs/closed/4347.v
@@ -0,0 +1,17 @@
+Fixpoint demo_recursion(n:nat) := match n with
+                                    |0 => Type
+                                    |S k => (demo_recursion k) -> Type
+                                    end.
+
+Record Demonstration := mkDemo
+{
+    demo_law : forall n:nat, demo_recursion n;
+    demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type :=
+     match n with
+     | 0 => Type
+     | S k => demo_recursion k -> Type
+     end) n, (demo_law (S n)) q
+}.
+
+Theorem DemoError : Demonstration.
+Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*)
diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v
new file mode 100644
index 00000000..e71ddaf7
--- /dev/null
+++ b/test-suite/bugs/closed/4354.v
@@ -0,0 +1,11 @@
+Inductive True : Prop := I.
+Class Lift (T : Type).
+Axiom closed_increment : forall {T} {H : Lift T}, True.
+Create HintDb core.
+Lemma closed_monotonic T (H : Lift T) : True.
+Proof.
+  Set Printing Universes.
+  auto using closed_increment. Show Universes.
+Qed.
+(* also fails with -nois, so the content of the hint database does not matter
+*)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
new file mode 100644
index 00000000..6a5e9a40
--- /dev/null
+++ b/test-suite/bugs/closed/4366.v
@@ -0,0 +1,15 @@
+Fixpoint stupid (n : nat) : unit :=
+match n with
+| 0 => tt
+| S n =>
+  let () := stupid n in
+  let () := stupid n in
+  tt
+end.
+
+Goal True.
+Proof.
+pose (v := stupid 24).
+Timeout 2 vm_compute in v.
+exact I.
+Qed.
diff --git a/test-suite/bugs/closed/4372.v b/test-suite/bugs/closed/4372.v
new file mode 100644
index 00000000..428192a3
--- /dev/null
+++ b/test-suite/bugs/closed/4372.v
@@ -0,0 +1,20 @@
+(* Tactic inversion was raising an anomaly because of a fake
+   dependency of TypeDenote into its argument *)
+
+Inductive expr :=
+| ETrue.
+
+Inductive IntermediateType : Set := ITbool.
+
+Definition TypeDenote (IT : IntermediateType) : Type :=
+  match IT with
+  | _ => bool
+  end.
+
+Inductive ValueDenote : forall (e:expr) it, TypeDenote it -> Prop :=
+| VT : ValueDenote ETrue ITbool true.
+
+Goal forall it v, @ValueDenote ETrue it v -> True.
+  intros it v H.
+  inversion H.
+Abort.
diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v
new file mode 100644
index 00000000..03af1653
--- /dev/null
+++ b/test-suite/bugs/closed/4375.v
@@ -0,0 +1,106 @@
+
+
+Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  t.
+
+
+Module A.
+Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  match n with
+  | 0 => t
+  | S n => bar t n
+  end
+
+with bar (t : Type@{i}) (n : nat) : Type@{i} :=
+    match n with
+    | 0 => t
+    | S n => foo t n
+    end.
+End A.
+
+Module B.
+Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  match n with
+  | 0 => t
+  | S n => bar t n
+  end
+
+with bar@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+    match n with
+    | 0 => t
+    | S n => foo t n
+    end.
+End B.
+
+Module C.
+Fail Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  match n with
+  | 0 => t
+  | S n => bar t n
+  end
+
+with bar@{j} (t : Type@{j}) (n : nat) : Type@{j} :=
+    match n with
+    | 0 => t
+    | S n => foo t n
+    end.
+End C.
+
+Module D.
+Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} :=
+  match n with
+  | 0 => t
+  | S n => bar t n
+  end
+
+with bar@{i j} (t : Type@{j}) (n : nat) : Type@{j} :=
+    match n with
+    | 0 => t
+    | S n => foo t n
+    end.
+End D.
+
+Module E.
+Fail Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} :=
+  match n with
+  | 0 => t
+  | S n => bar t n
+  end
+
+with bar@{j i} (t : Type@{j}) (n : nat) : Type@{j} :=
+    match n with
+    | 0 => t
+    | S n => foo t n
+    end.
+End E.
+
+(*
+Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  t.
+
+Print g.
+
+Polymorphic Fixpoint a@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  t
+with b@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
+  t.
+
+Print a.
+Print b.
+*)
+
+Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} :=
+| A : foo T -> foo T.
+
+Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t :=
+  @A@{i} t (cg@{i} t).
+
+Print cg.
+
+Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t :=
+  @A@{i} t (@cb@{i} t)
+with cb@{i} (t : Type@{i}) : foo@{i} t :=
+  @A@{i} t (@ca@{i} t).
+
+Print ca.
+Print cb.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
new file mode 100644
index 00000000..a96a1370
--- /dev/null
+++ b/test-suite/bugs/closed/4390.v
@@ -0,0 +1,37 @@
+Module A.
+Set Printing All.
+Set Printing Universes.
+
+Module M.
+Section foo.
+Universe i.
+End foo.
+End M.
+
+Check Type@{i}.
+(* Succeeds *)
+
+Fail Check Type@{j}.
+(* Error: Undeclared universe: j *)
+
+Definition foo@{j} : Type@{i} := Type@{j}.
+(* ok *)
+End A.
+
+Set Universe Polymorphism.
+Fail Universes j.
+Monomorphic Universe j.
+Section foo.
+  Universes i.
+  Constraint i < j.
+  Definition foo : Type@{j} := Type@{i}.
+  Definition foo' : Type@{j} := Type@{i}.
+End foo.
+
+Check eq_refl : foo@{i} = foo'@{i}.
+
+Definition bar := foo.
+Monomorphic Definition bar'@{k} := foo@{k}.
+
+Fail Constraint j = j.
+Monomorphic Constraint i = i.
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
new file mode 100644
index 00000000..60c93545
--- /dev/null
+++ b/test-suite/bugs/closed/4394.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Require Import Equality List.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
+
diff --git a/test-suite/bugs/closed/4397.v b/test-suite/bugs/closed/4397.v
new file mode 100644
index 00000000..3566353d
--- /dev/null
+++ b/test-suite/bugs/closed/4397.v
@@ -0,0 +1,3 @@
+Require Import Equality.
+Theorem foo (u : unit) (H : u = u) : True.
+dependent destruction H.
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 0b8bb235..844ff875 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Module Comment1.
   Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index ae3e50d7..223a98de 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -3,9 +3,9 @@ Set Implicit Arguments.
 Generalizable All Variables.
 Set Universe Polymorphism.
 
-Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
-  Object :> _ := obj;
-  Morphism' : obj -> obj -> Type;
+Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' {
+  Object :> Type@{l} := obj;
+  Morphism' : obj -> obj -> Type@{k};
 
   Identity' : forall o, Morphism' o o;
   Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index 4c3e078a..7a84531a 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module Version1.
   Set Implicit Arguments.
   Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index a14fb6aa..e2bf1dbe 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_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index b7db22a6..90d1d183 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index 38943ab3..4f8868d5 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
 Set Printing All.
 Set Printing Implicit.
@@ -21,7 +22,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 4f5ef997..b6c0da76 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/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
new file mode 100644
index 00000000..e46ea58b
--- /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). *)