1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/closed/HoTT_coq_083.v
new file mode 100644
index 00000000..494b25c7
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_083.v
@@ -0,0 +1,29 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob : Type }.
+
+Goal forall C, ob C -> ob C.
+intros.
+generalize dependent (ob C).
+(* 1 subgoals, subgoal 1 (ID 7)
+
+  C : category
+  ============================
+   forall T : Type, T -> T
+(dependent evars:) *)
+intros T t.
+Undo 2.
+generalize dependent (@ob C).
+(* 1 subgoals, subgoal 1 (ID 6)
+
+  C : category
+  X : ob C
+  ============================
+   Type -> ob C
+(dependent evars:) *)
+intros T t.
+(* Toplevel input, characters 9-10:
+Error: No product even after head-reduction. *)