File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7: Error: Signature components for label test do not match: expected type "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".