Add regression tests for univ. poly. and prim proj

These 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 passes.

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

diff --git a/test-suite/bugs/closed/3205.v b/test-suite/bugs/closed/3205.v
new file mode 100644
index 000000000..5c44f0703
--- /dev/null
+++ b/test-suite/bugs/closed/3205.v
@@ -0,0 +1,26 @@
+Fail Fixpoint F (u : unit) : Prop :=
+  (fun p : {P : Prop & _} => match p with existT _ _ P => P end)
+  (existT (fun P => False -> P) (F tt) _).
+(* Anomaly: A universe comparison can only happen between variables.
+Please report. *)
+
+
+
+Definition g (x : Prop) := x.
+
+Definition h (y : Type) := y.
+
+Definition eq_hf : h = g :> (Prop -> Type) :=
+  @eq_refl (Prop -> Type) g.
+
+Set Printing All.
+Set Printing Universes.
+Fail Definition eq_hf : h = g :> (Prop -> Type) :=
+  eq_refl g.
+(* Originally an anomaly, now says
+Toplevel input, characters 48-57:
+Error:
+The term "@eq_refl (forall _ : Prop, Prop) g" has type
+ "@eq (forall _ : Prop, Prop) g g" while it is expected to have type
+ "@eq (forall _ : Prop, Type (* Top.16 *)) (fun y : Prop => h y) g"
+(Universe inconsistency: Cannot enforce Prop = Top.16)). *)