Add more regression tests for univ poly/prim proj

hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.

These are the tests that trunk currently fails.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v
new file mode 100644
index 000000000..72b4ffe94
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_102.v
@@ -0,0 +1,23 @@
+(* File reduced by coq-bug-finder from 64 lines to 30 lines. *)
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+Record SpecializedCategory (obj : Type) := { Object :> _ := obj }.
+
+Record > Category :=
+  { CObject : Type;
+    UnderlyingCategory :> @SpecializedCategory CObject }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  { ObjectOf :> objC -> objD }.
+
+Definition Functor (C D : Category) := SpecializedFunctor C D.
+
+Parameter TerminalCategory : SpecializedCategory unit.
+
+Definition focus A (_ : A) := True.
+
+Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
+  assert (Hf : focus ((S tt) = (S tt))) by constructor.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  (* not convertible *)