1 files changed, 0 insertions, 29 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/closed/HoTT_coq_083.v
deleted file mode 100644
index 494b25c7b..000000000
--- a/test-suite/bugs/closed/HoTT_coq_083.v
+++ /dev/null
@@ -1,29 +0,0 @@
-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. *)