aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/IntMap/Allmaps.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/IntMap/Allmaps.v')
-rw-r--r--theories/IntMap/Allmaps.v18
1 files changed, 18 insertions, 0 deletions
diff --git a/theories/IntMap/Allmaps.v b/theories/IntMap/Allmaps.v
new file mode 100644
index 000000000..89520483b
--- /dev/null
+++ b/theories/IntMap/Allmaps.v
@@ -0,0 +1,18 @@
+
+Require Export Addr.
+Require Export Adist.
+Require Export Addec.
+Require Export Map.
+
+Require Export Fset.
+Require Export Mapaxioms.
+Require Export Mapiter.
+
+Require Export Mapsubset.
+Require Export Lsort.
+Require Export Mapfold.
+Require Export Mapcard.
+Require Export Mapcanon.
+Require Export Mapc.
+Require Export Maplists.
+Require Export Adalloc.