aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3974.v
blob: b166e73fa16c974f53872c794177615fca736d4d (plain)
1
2
3
4
5
6
7
8
Module Type S.
End S.

Module Type M (X : S).
  Fail Module P (X : S).
  (* Used to say: Anomaly: X already exists. Please report. *)
  (* Should rather say now: Error: X already exists. *)
End M.