aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Reordering.v
blob: e79b20737b554e54307aec293e059c03018efa6f (plain)
1
2
3
4
5
(* Testing that hypothesis order (following a conversion/folding) is checked *)

Goal forall (A:Set) (x:A) (A':=A), True.
intros.
Fail change ((fun (_:A') => Set) x) in (type of A).