blob: 7b6696af8e41ba5ff760fddeaa828235251838f0 (
plain)
1
2
3
4
5
|
(* An example showing a bug in the detection of free variables *)
(* "x" is not free in the common type of "x" and "y" *)
Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
|
