5 files changed, 61 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v
new file mode 100644
index 0000000000..d7fc2aaa00
--- /dev/null
+++ b/test-suite/bugs/closed/5449.v
@@ -0,0 +1,6 @@
+(* An example of decide equality which was failing due to a lhs dep into the rhs *)
+
+Require Import Coq.PArith.BinPos.
+Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}.
+intros.
+decide equality.
diff --git a/test-suite/bugs/closed/5501.v b/test-suite/bugs/closed/5501.v
new file mode 100644
index 0000000000..24739a3658
--- /dev/null
+++ b/test-suite/bugs/closed/5501.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+
+Record Pred@{A} :=
+  { car :> Type@{A}
+  ; P : car -> Prop
+  }.
+
+Class All@{A} (A : Pred@{A}) : Type :=
+  { proof : forall (a : A), P A a
+  }.
+
+Record Pred_All@{A} : Type :=
+  { P' :> Pred@{A}
+  ; P'_All : All P'
+  }.
+
+Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
+
+Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
+Proof.
+solve[auto using proof].
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index b62f9b6867..bb9579d487 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,6 +1,5 @@
-(* This was working in version 8.1beta (bug in the Sort-polymorphism
-   of inductive types), but this is inconsistent with classical logic
-   in Prop *)
+(* This was working in version 8.1beta (bug in template polymorphism),
+   but this is inconsistent with classical logic in Prop *)
 
 Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
 with bool : Type := true : bool | false : bool.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index c29e529783..e59828defe 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -1,5 +1,5 @@
 (* This used to fail in Coq version 8.1 beta due to a non variable
-   universe (issued by the inductive sort-polymorphism) being sent by
+   universe (issued by template polymorphism) being sent by
    pretyping to the kernel (bug #1182) *)
 
 Variable T : Type.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd92..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
 Type)) eq_refl.
 
-End Hurkens'.
-\ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+  Set Universe Polymorphism.
+
+  Definition defaultid := (fun x => x) : Type -> Type.
+  Definition collapseid := defaultid@{_ _}.
+  Check collapseid@{_}.
+
+  Definition anonid := (fun x => x) : Type -> Type@{_}.
+  Check anonid@{_}.
+
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
+  Check usedefaultalg@{_ _}.
+
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
+
+  Definition unrelated@{i j} := nat.
+  Definition useunrelated := unrelated@{_ _}.
+  Check useunrelated@{_ _}.
+
+  Definition inthemiddle@{i j k} :=
+    let _ := defaultid@{i j} in
+    anonalg@{k j}.
+  (* i <= j < k *)
+  Definition collapsethemiddle := inthemiddle@{i _ j}.
+  Check collapsethemiddle@{_ _}.
+
+End Anonymous.