aboutsummaryrefslogtreecommitdiff
path: root/lib/lib.mllib
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-27 10:19:21 +0100
committerMaxime Dénès2017-12-27 10:19:21 +0100
commit4969f9425cb0d5cd5bd735110886a0cbd2641588 (patch)
tree6c05276df78dd476642ab5db8437e8730d19eb56 /lib/lib.mllib
parent3921ff2e2c189063ec46f54cbb247570b6c59b2c (diff)
parent5ffa147bd2fe548df3ac9053fe497d0871a5f6df (diff)
Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.
Diffstat (limited to 'lib/lib.mllib')
-rw-r--r--lib/lib.mllib39
1 files changed, 24 insertions, 15 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 66f939a910..b2260ba097 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,21 +1,30 @@
+Coq_config
+
+Hook
+Flags
+Control
+Util
+
+Pp
+Stateid
+Loc
+Feedback
CErrors
CWarnings
-Bigint
-Segmenttree
-Unicodetable
-Unicode
-Minisys
+
+Rtree
System
-CThread
-Spawn
-Trie
-CProfile
Explore
-Predicate
-Rtree
-Heap
-Unionfind
-Genarg
-CEphemeron
+RTree
+CProfile
Future
+Spawn
+
+CAst
+DAst
+Genarg
+
RemoteCounter
+Aux_file
+Envars
+CoqProject_file