summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2668.v
blob: 74c8fa347bb0f3cae29c7dad8eb093de125a0c91 (plain)
1
2
3
4
5
6
Require Import MSetPositive.
Require Import MSetProperties.

Module Pos := MSetPositive.PositiveSet.
Module PPPP := MSetProperties.WPropertiesOn(Pos).
Print Module PPPP.