rewrite_in_goal.v « failure « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/failure/rewrite_in_goal.v

blob: e7823f1cb189c95a8af42fe2f9568c6243bf2913 (plain)

Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type.
  intros until x.
  Fail rewrite H in x.
Abort.