summaryrefslogtreecommitdiff
path: root/test-suite/prerequisite/module_bug8416.v
blob: 70f43d132addea47d526a0bd50e8038a6af6d57c (plain)
1
2
Module Type A. Axiom f : True. End A.
Module M8416 : A. Definition f := I. End M8416.