aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2920.v
blob: 13548b9e44c94fa9cd424c1993717e7695e941c2 (plain)
1
2
Fail Definition my_f_equal {A B : Type} (f : A -> B) (a a' : A) (p : a = a') : f a = f a' :=
  eq_ind _ _ (fun a' => f a = f a') _ _ p.