aboutsummaryrefslogtreecommitdiff
path: root/theories/MMaps/MMaps.v
diff options
context:
space:
mode:
authorPierre Letouzey2015-03-06 12:13:28 +0100
committerPierre Letouzey2015-03-06 12:16:12 +0100
commitcd84370dfc402ca96ba677a36fb8b6e8c0ae09a0 (patch)
tree06ecd901e36f3f00c8413a60cfc049ca994a9d99 /theories/MMaps/MMaps.v
parent5f3e713778ecde8c6f9cd7d8104860e49655de32 (diff)
MMapPositive: another implementation of MMaps
Diffstat (limited to 'theories/MMaps/MMaps.v')
-rw-r--r--theories/MMaps/MMaps.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/MMaps/MMaps.v b/theories/MMaps/MMaps.v
index 609cbffbb8..054d07225a 100644
--- a/theories/MMaps/MMaps.v
+++ b/theories/MMaps/MMaps.v
@@ -13,6 +13,4 @@ Require Export MMapInterface.
Require Export MMapFacts.
Require Export MMapWeakList.
Require Export MMapList.
-(*
Require Export MMapPositive.
-*) \ No newline at end of file