summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3974.v
blob: 3d9e06b6120852419fafb783405e5af84767b659 (plain)
1
2
3
4
5
6
7
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. *)