bug_12909.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_12909.v

blob: fafb6a418fa3cbacddfd00ea277c3c3e0e1a6239 (plain)

Module Type T.
Axiom A : Type.
End T.

Module M.
  Axiom A : SProp.
End M.
Fail Module N <: T := M.