aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2616.v
blob: 8758e32dd83654f333b5398062168295068edb23 (plain)
1
2
3
4
5
6
7
(* Testing ill-typed rewrite which used to succeed in 8.3 *)
Goal 
  forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), 
    N 0 -> False.
Proof.
intros.
Fail rewrite IN in H.