test-suite/bugs/closed/bug_5752.v


1
2
3
4
5
6
7
8

Class C (A : Type) := c : A.

Hint Mode C ! : typeclass_instances.

Goal forall f : (forall A, C A -> C (list A)), True.
intros.
  Check c. (* Loops if modes are ignored. *)
Abort.