aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/stdlib/index-list.html.template22
-rw-r--r--toplevel/coqinit.ml1
2 files changed, 0 insertions, 23 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index aa725b9487..c86338175e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -307,27 +307,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Wellfounded/Well_Ordering.v
</dd>
-
- <dt> <b>IntMap</b>:
- An implementation of finite sets/maps as trees indexed by
- addresses (obsolete, supersided by FSets/FMap)
- </dt>
- <dd>
- theories/IntMap/Adalloc.v
- theories/IntMap/Map.v
- theories/IntMap/Fset.v
- theories/IntMap/Mapaxioms.v
- theories/IntMap/Mapiter.v
- theories/IntMap/Mapcanon.v
- theories/IntMap/Mapsubset.v
- theories/IntMap/Lsort.v
- theories/IntMap/Mapfold.v
- theories/IntMap/Mapcard.v
- theories/IntMap/Mapc.v
- theories/IntMap/Maplists.v
- theories/IntMap/Allmaps.v
- </dd>
-
<dt> <b>FSets</b>:
Modular implementation of finite sets/maps using lists or
efficient trees
@@ -349,7 +328,6 @@ through the <tt>Require Import</tt> command.</p>
theories/FSets/FMapInterface.v
theories/FSets/FMapList.v
theories/FSets/FMapPositive.v
- theories/FSets/FMapIntMap.v
theories/FSets/FMapFacts.v
(theories/FSets/FMaps.v)
theories/FSets/FMapAVL.v
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 95ffeb44af..10d64dcf80 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -74,7 +74,6 @@ let theories_dirs_map = [
"theories/Classes", "Classes" ;
"theories/Program", "Program" ;
"theories/FSets", "FSets" ;
- "theories/IntMap", "IntMap" ;
"theories/Reals", "Reals" ;
"theories/Strings", "Strings" ;
"theories/Sorting", "Sorting" ;