test-suite/bugs/closed/3017.v


1
2
3
4
5
6

Class A := {}.
  Class B {T} `(A) := { B_intro : forall t t' : T, t = t' }.
  Lemma foo T (t t' : T) : t = t'.
    erewrite @B_intro.
    reflexivity.
  Abort.