names.v « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/names.v

blob: b3b5071a032d26ee2190cfa3b0018b9ee904d7d4 (plain)

(* 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.