aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3017.v
blob: 63a06bd3d6b7c730cf64a83533e24865fe24540a (plain)
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.