aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/rewrite_in_hyp.v
blob: 1eef0fa0333bc544e1fe6c31b26b4e134e692c65 (plain)
1
2
3
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.