aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/rewrite_in_goal.v
blob: c11a6237c5a96a3d9c219606a4735ff46ae240d8 (plain)
1
2
3
Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type.
  intros until x.
  rewrite H in x.