rewrite_in_goal.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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.