1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_082.v b/test-suite/bugs/closed/HoTT_coq_082.v
new file mode 100644
index 00000000..ccba22ca
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_082.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob : Type }.
+
+Existing Class category. (*
+Toplevel input, characters 0-24:
+Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
+
+Record category' :=
+  { ob' : Type;
+    hom' : ob' -> ob' -> Type }.
+
+Existing Class category'. (*
+Toplevel input, characters 0-24:
+Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)