rewrite_in_goal.v « failure « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: dedfdf01eb2c3b1cd155f77c4e2ada7806f74738 (plain)

1
2
3

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