5 files changed, 147 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v
new file mode 100644
index 000000000..ecebaba81
--- /dev/null
+++ b/test-suite/bugs/closed/4450.v
@@ -0,0 +1,58 @@
+Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop.
+
+Polymorphic Axiom unit@{u} : Type@{u}.
+Polymorphic Axiom tt@{u} : inhabited unit@{u}.
+
+Polymorphic Hint Resolve tt : the_lemmas.
+Set Printing All.
+Set Printing Universes.
+Goal inhabited unit.
+Proof.
+  eauto with the_lemmas.
+Qed.
+
+Universe u.
+Axiom f : Type@{u} -> Prop.
+Lemma fapp (X : Type) : f X -> False.
+Admitted.
+Polymorphic Axiom funi@{i} : f unit@{i}.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto using (fapp unit funi). (* The two fapp's have different universes *)
+Qed.
+
+Hint Resolve (fapp unit funi) : mylems.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto with mylems. (* Forces the two fapps at the same level *)
+Qed.
+
+Goal (forall U, f U) -> (f unit -> False) -> False /\ False.
+  eauto. (* Forces the two fapps at the same level *)
+Qed.
+
+Polymorphic Definition MyType@{i} := Type@{i}.
+Universes l m n.
+Constraint l < m.
+Polymorphic Axiom maketype@{i} : MyType@{i}.
+
+Goal MyType@{l}.
+Proof.
+  Fail solve [ eauto using maketype@{m} ].
+  eauto using maketype.
+  Undo.
+  eauto using maketype@{n}.
+Qed.
+
+Axiom foo : forall (A : Type), list A.
+Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
+
+Universe x y.
+Goal list Type@{x}.
+Proof.
+  eauto using (foo Type). (* Refreshes the term *)
+  Undo.
+  eauto using foo. Show Universes.
+  Undo.
+  eauto using foop. Show Proof. Show Universes.
+Qed.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v
new file mode 100644
index 000000000..fd5e0fb60
--- /dev/null
+++ b/test-suite/bugs/closed/4725.v
@@ -0,0 +1,38 @@
+Require Import EquivDec Equivalence List Program.
+Require Import Relation_Definitions.
+Import ListNotations.
+Generalizable All Variables.
+
+Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V
+:=
+  match l with
+  | nil => nil
+  | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl)
+  end.
+
+Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
+@EqDec V eqV equivV} (xs : list V) (x : V) :
+  length (removeV x xs) < length (x :: xs).
+  Proof. Admitted.
+
+(* Function version *)
+Set Printing Universes.
+
+Require Import Recdef.
+
+Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
+@EqDec V eqV equivV} (l : list V) { measure length l} :=
+    match l with
+      | nil => nil
+      | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs)
+    end.
+Proof. intros. apply remove_le. Qed.
+
+(* Program version *)
+
+Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V)
+        {  measure (@length V l) lt } :=
+    match l with
+      | nil => nil
+      | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _
+    end.
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index ed4443786..dbd71035d 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
  
+(* A simplification of an example from coquelicot, which was failing
+   at some time after a fix #4782 was committed. *)
+
+Record T := { dom : Type }.
+Definition pairT A B := {| dom := (dom A * dom B)%type |}.
+Class C (A:Type).
+Parameter B:T.
+Instance c (A:T) : C (dom A).
+Instance cn : C (dom B).
+Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
+Set Typeclasses Debug.
+Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
+intros.
+apply (F _ _)  with (x,x).
+  
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
index 86597c88f..00a523842 100644
--- a/test-suite/bugs/closed/4816.v
+++ b/test-suite/bugs/closed/4816.v
@@ -15,3 +15,15 @@ Section Foo.
     Fail Constraint X <= Z.
   End Bar.
 End Foo.
+
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+Section qux.
+  Polymorphic Universes A.
+  Section bar.
+    Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+  End bar.
+End qux.
diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v
new file mode 100644
index 000000000..904abb228
--- /dev/null
+++ b/test-suite/bugs/closed/4818.v
@@ -0,0 +1,24 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *)
+(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3
+   coqtop version 8.5pl1 (June 2016) *)
+Set Universe Polymorphism.
+
+Inductive GCov (I : Type) : Type := | Foo : I -> GCov I.
+
+Section Product.
+
+Variables S IS : Type.
+Variable locS : IS -> True.
+
+Goal GCov (IS * S) -> GCov IS.
+intros X0. induction X0; intros.
+destruct i.
+specialize (locS i).
+clear -locS. 
+destruct locS. Show Universes.
+Admitted.
+
+(*
+Anomaly: Universe Product.5189 undefined. Please report.
+*)