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

about summary refs log tree commit diff

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

blob: f1b2203acc3275b322a835793cddadf7789047bd (plain)

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