From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- test-suite/bugs/closed/shouldsucceed/2668.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/shouldsucceed/2668.v (limited to 'test-suite/bugs/closed/shouldsucceed/2668.v') diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v new file mode 100644 index 00000000..74c8fa34 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2668.v @@ -0,0 +1,6 @@ +Require Import MSetPositive. +Require Import MSetProperties. + +Module Pos := MSetPositive.PositiveSet. +Module PPPP := MSetProperties.WPropertiesOn(Pos). +Print Module PPPP. \ No newline at end of file -- cgit v1.2.3