aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/names.v
blob: b3b5071a032d26ee2190cfa3b0018b9ee904d7d4 (plain)
1
2
3
4
5
(* Test no clash names occur *)
(* see bug #2723 *)

Parameter a : forall x, {y:nat|x=y}.
Fail Definition b y : {x:nat|x=y} := a y.