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, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
new file mode 100644
index 000000000..39a7103d1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -0,0 +1,22 @@
+(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope category_scope.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+(* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)