[lib] Split auxiliary libraries into Coq-specific and general.

Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.

We know split the directory in two, as to make the distinction clear:

- `clib`: contains libraries that are not Coq specific and implement
  common data structures and programming patterns. These libraries
  could be eventually replace with external dependencies and the rest
  of the code base wouldn't notice much.

- `lib`: contains Coq-specific common libraries in widespread use
  along the codebase, but that are not considered part of other
  components. Examples are printing, error handling, or flags.

In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.

Also note that `Deque` is not used ATM.

74 files changed, 102 insertions, 83 deletions

diff --git a/.merlin b/.merlin
index 21555f5e5..d60f5037b 100644
--- a/.merlin
+++ b/.merlin
@@ -1,17 +1,17 @@
 FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50
 
+S clib
+B clib
 S config
 B config
-S ide
-B ide
 S lib
 B lib
-S intf
-B intf
 S kernel
 B kernel
 S kernel/byterun
 B kernel/byterun
+S intf
+B intf
 S library
 B library
 S engine
@@ -30,14 +30,16 @@ S parsing
 B parsing
 S stm
 B stm
-S toplevel
-B toplevel
 S vernac
 B vernac
+S toplevel
+B toplevel
 S plugins/ltac
 B plugins/ltac
 S API
 B API
+S ide
+B ide
 
 S tools
 B tools
diff --git a/META.coq b/META.coq
index d31b60cd0..75cec8f0c 100644
--- a/META.coq
+++ b/META.coq
@@ -23,19 +23,27 @@ package "config" (
 
 )
 
+package "clib" (
+  description = "Base General Coq Library"
+  version     = "8.7"
+
+  directory   = "clib"
+  requires    = "str, unix, threads"
+
+  archive(byte)    = "clib.cma"
+  archive(native)  = "clib.cmxa"
+)
+
 package "lib" (
 
-  description = "Base Coq Library"
+  description = "Base Coq-Specific Library"
   version     = "8.7"
 
   directory   = "lib"
 
-  requires         = "str, unix, threads, coq.config"
+  requires    = "coq.clib, coq.config"
 
-  archive(byte)    = "clib.cma"
   archive(byte)   += "lib.cma"
-
-  archive(native)  = "clib.cmxa"
   archive(native) += "lib.cmxa"
 
 )
diff --git a/Makefile.build b/Makefile.build
index 2f7ce6ef3..33ab72e68 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 COQOPTS=$(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
-LOCALINCLUDES=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
+LOCALINCLUDES=$(if $(filter plugins/%,$@),-I clib -I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
@@ -417,7 +417,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
 
 # coqc
 
-COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
+COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
 
 $(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -438,21 +438,21 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
 # Remember to update the dependencies below when you add files!
 
 COQDEPBOOTSRC := \
- lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
+ clib/segmenttree.cmo clib/unicodetable.cmo clib/unicode.cmo clib/minisys.cmo \
  tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo
 
-lib/segmenttree.cmo : lib/segmenttree.cmi
-lib/segmenttree.cmx : lib/segmenttree.cmi
-lib/unicodetable.cmo : lib/segmenttree.cmo
-lib/unicodetable.cmx : lib/segmenttree.cmx
-lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi
-lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi
-lib/minisys.cmo : lib/unicode.cmo
-lib/minisys.cmx : lib/unicode.cmx
-tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi
-tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi
-tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
-tools/coqdep_common.cmx : lib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi
+clib/segmenttree.cmo : clib/segmenttree.cmi
+clib/segmenttree.cmx : clib/segmenttree.cmi
+clib/unicodetable.cmo : clib/segmenttree.cmo
+clib/unicodetable.cmx : clib/segmenttree.cmx
+clib/unicode.cmo : clib/unicodetable.cmo clib/unicode.cmi
+clib/unicode.cmx : clib/unicodetable.cmx clib/unicode.cmi
+clib/minisys.cmo : clib/unicode.cmo
+clib/minisys.cmx : clib/unicode.cmx
+tools/coqdep_lexer.cmo : clib/unicode.cmi tools/coqdep_lexer.cmi
+tools/coqdep_lexer.cmx : clib/unicode.cmx tools/coqdep_lexer.cmi
+tools/coqdep_common.cmo : clib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
+tools/coqdep_common.cmx : clib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi
 tools/coqdep_boot.cmo : tools/coqdep_common.cmi
 tools/coqdep_boot.cmx : tools/coqdep_common.cmx
 
@@ -466,10 +466,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \
-  lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \
-  lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \
-  tools/coqdep.cmo
+COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo	\
+  tools/coqdep_common.cmo tools/coqdep.cmo
 
 $(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -479,7 +477,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,)
 
-COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo
+COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -493,23 +491,24 @@ $(COQWC): $(call bestobj, tools/coqwc.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str)
 
-COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
+COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
 $(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str,unix)
 
-$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
+$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo	ide/document.cmo \
- ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \
- ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
+ ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo	\
+ ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo	\
+ tools/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -517,7 +516,7 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
+bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker)
 
@@ -525,7 +524,7 @@ bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo
 # Csdp to micromega special targets
 ###########################################################################
 
-CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \
+CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
@@ -581,7 +580,7 @@ kernel/kernel.cma: kernel/kernel.mllib
 # Make sure that API/API.mli cannot leak types from the Coq codebase.
 API/API.cmi : API/API.mli
 	$(SHOW)'OCAMLC    $<'
-	$(HIDE)$(OCAMLC) -I lib -I $(MYCAMLP4LIB) -c $<
+	$(HIDE)$(OCAMLC) -I clib -I lib -I $(MYCAMLP4LIB) -c $<
 
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
diff --git a/Makefile.checker b/Makefile.checker
index 7e0f58875..5b5855782 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -20,7 +20,7 @@ CHICKEN:=bin/coqchk$(EXE)
 
 # The sources
 
-CHKLIBS:= -I config -I lib -I checker
+CHKLIBS:= -I config -I clib -I lib -I checker
 
 ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
 
diff --git a/Makefile.common b/Makefile.common
index f436d3e8f..7e8f3e3e7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -73,7 +73,7 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 CORESRCDIRS:=\
-  config 	lib		kernel	intf	kernel/byterun	library \
+  config 	clib 		lib		kernel	intf	kernel/byterun	library \
   engine 	pretyping	interp	proofs	parsing 	printing \
   tactics 	vernac		stm		toplevel 	API
 
@@ -100,7 +100,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
+CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
 	stm/stm.cma toplevel/toplevel.cma API/API.cma
diff --git a/Makefile.ide b/Makefile.ide
index 7d809f67a..08829b554 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -41,7 +41,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
-IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo
+IDEDEPS:=clib/clib.cma lib/lib.cma
 IDECMA:=ide/ide.cma
 IDETOPLOOPCMA=ide/coqidetop.cma
 
diff --git a/lib/backtrace.ml b/clib/backtrace.ml
index be9f40c1f..be9f40c1f 100644
--- a/lib/backtrace.ml
+++ b/clib/backtrace.ml
diff --git a/lib/backtrace.mli b/clib/backtrace.mli
index dd82165b6..dd82165b6 100644
--- a/lib/backtrace.mli
+++ b/clib/backtrace.mli
diff --git a/lib/bigint.ml b/clib/bigint.ml
index 4f8b95d59..4f8b95d59 100644
--- a/lib/bigint.ml
+++ b/clib/bigint.ml
diff --git a/lib/bigint.mli b/clib/bigint.mli
index 2a5a5f122..2a5a5f122 100644
--- a/lib/bigint.mli
+++ b/clib/bigint.mli
diff --git a/lib/cArray.ml b/clib/cArray.ml
index 013585735..013585735 100644
--- a/lib/cArray.ml
+++ b/clib/cArray.ml
diff --git a/lib/cArray.mli b/clib/cArray.mli
index 325ff8edc..325ff8edc 100644
--- a/lib/cArray.mli
+++ b/clib/cArray.mli
diff --git a/lib/cEphemeron.ml b/clib/cEphemeron.ml
index 8b253a790..8b253a790 100644
--- a/lib/cEphemeron.ml
+++ b/clib/cEphemeron.ml
diff --git a/lib/cEphemeron.mli b/clib/cEphemeron.mli
index d8a1f2757..d8a1f2757 100644
--- a/lib/cEphemeron.mli
+++ b/clib/cEphemeron.mli
diff --git a/lib/cList.ml b/clib/cList.ml
index 0ef7c3d8b..0ef7c3d8b 100644
--- a/lib/cList.ml
+++ b/clib/cList.ml
diff --git a/lib/cList.mli b/clib/cList.mli
index f87db04cf..f87db04cf 100644
--- a/lib/cList.mli
+++ b/clib/cList.mli
diff --git a/lib/cMap.ml b/clib/cMap.ml
index b4c4aedd0..b4c4aedd0 100644
--- a/lib/cMap.ml
+++ b/clib/cMap.ml
diff --git a/lib/cMap.mli b/clib/cMap.mli
index 5e65bd200..5e65bd200 100644
--- a/lib/cMap.mli
+++ b/clib/cMap.mli
diff --git a/lib/cObj.ml b/clib/cObj.ml
index 7f3ee1855..7f3ee1855 100644
--- a/lib/cObj.ml
+++ b/clib/cObj.ml
diff --git a/lib/cObj.mli b/clib/cObj.mli
index 16933a4aa..16933a4aa 100644
--- a/lib/cObj.mli
+++ b/clib/cObj.mli
diff --git a/lib/cSet.ml b/clib/cSet.ml
index ed65edf16..ed65edf16 100644
--- a/lib/cSet.ml
+++ b/clib/cSet.ml
diff --git a/lib/cSet.mli b/clib/cSet.mli
index 2eb9bce86..2eb9bce86 100644
--- a/lib/cSet.mli
+++ b/clib/cSet.mli
diff --git a/lib/cSig.mli b/clib/cSig.mli
index 32e9d2af0..32e9d2af0 100644
--- a/lib/cSig.mli
+++ b/clib/cSig.mli
diff --git a/lib/cStack.ml b/clib/cStack.ml
index 4acb2930c..4acb2930c 100644
--- a/lib/cStack.ml
+++ b/clib/cStack.ml
diff --git a/lib/cStack.mli b/clib/cStack.mli
index 8dde1d1a1..8dde1d1a1 100644
--- a/lib/cStack.mli
+++ b/clib/cStack.mli
diff --git a/lib/cString.ml b/clib/cString.ml
index f2242460e..f2242460e 100644
--- a/lib/cString.ml
+++ b/clib/cString.ml
diff --git a/lib/cString.mli b/clib/cString.mli
index 29d3a4499..29d3a4499 100644
--- a/lib/cString.mli
+++ b/clib/cString.mli
diff --git a/lib/cThread.ml b/clib/cThread.ml
index 0221e690e..0221e690e 100644
--- a/lib/cThread.ml
+++ b/clib/cThread.ml
diff --git a/lib/cThread.mli b/clib/cThread.mli
index 66f039bb5..66f039bb5 100644
--- a/lib/cThread.mli
+++ b/clib/cThread.mli
diff --git a/lib/cUnix.ml b/clib/cUnix.ml
index 34fb660db..34fb660db 100644
--- a/lib/cUnix.ml
+++ b/clib/cUnix.ml
diff --git a/lib/cUnix.mli b/clib/cUnix.mli
index d08dc4c40..d08dc4c40 100644
--- a/lib/cUnix.mli
+++ b/clib/cUnix.mli
diff --git a/lib/canary.ml b/clib/canary.ml
index 0ed1d28f3..0ed1d28f3 100644
--- a/lib/canary.ml
+++ b/clib/canary.ml
diff --git a/lib/canary.mli b/clib/canary.mli
index 904b88213..904b88213 100644
--- a/lib/canary.mli
+++ b/clib/canary.mli
diff --git a/lib/clib.mllib b/clib/clib.mllib
index 5c1f7d9af..bd5ddb152 100644
--- a/lib/clib.mllib
+++ b/clib/clib.mllib
@@ -1,37 +1,38 @@
-Coq_config
-
-Terminal
 Canary
-Hook
+CObj
+CEphemeron
+
 Hashset
 Hashcons
+
 CSet
 CMap
+CList
+CString
+CStack
+
 Int
-Dyn
 HMap
+Bigint
+
+CArray
 Option
+CUnix
+
+Segmenttree
+Unicodetable
+Unicode
+Minisys
+CThread
+Trie
+Predicate
+Heap
+Unionfind
+
+Dyn
 Store
 Exninfo
 Backtrace
 IStream
-Flags
-Control
-Loc
-CAst
-DAst
-CList
-CString
-Deque
-CObj
-CArray
-CStack
-Util
-Stateid
-Pp
-Feedback
-CUnix
-Envars
-Aux_file
+Terminal
 Monad
-CoqProject_file
diff --git a/lib/deque.ml b/clib/deque.ml
index 373269b4f..373269b4f 100644
--- a/lib/deque.ml
+++ b/clib/deque.ml
diff --git a/lib/deque.mli b/clib/deque.mli
index 23cb1e491..23cb1e491 100644
--- a/lib/deque.mli
+++ b/clib/deque.mli
diff --git a/lib/dyn.ml b/clib/dyn.ml
index 64535d35f..64535d35f 100644
--- a/lib/dyn.ml
+++ b/clib/dyn.ml
diff --git a/lib/dyn.mli b/clib/dyn.mli
index 2206394e2..2206394e2 100644
--- a/lib/dyn.mli
+++ b/clib/dyn.mli
diff --git a/lib/exninfo.ml b/clib/exninfo.ml
index 167d3d6dc..167d3d6dc 100644
--- a/lib/exninfo.ml
+++ b/clib/exninfo.ml
diff --git a/lib/exninfo.mli b/clib/exninfo.mli
index c960ac7c0..c960ac7c0 100644
--- a/lib/exninfo.mli
+++ b/clib/exninfo.mli
diff --git a/lib/hMap.ml b/clib/hMap.ml
index 37079af78..37079af78 100644
--- a/lib/hMap.ml
+++ b/clib/hMap.ml
diff --git a/lib/hMap.mli b/clib/hMap.mli
index c77bfced8..c77bfced8 100644
--- a/lib/hMap.mli
+++ b/clib/hMap.mli
diff --git a/lib/hashcons.ml b/clib/hashcons.ml
index ee2232581..ee2232581 100644
--- a/lib/hashcons.ml
+++ b/clib/hashcons.ml
diff --git a/lib/hashcons.mli b/clib/hashcons.mli
index fbd2ebcf9..fbd2ebcf9 100644
--- a/lib/hashcons.mli
+++ b/clib/hashcons.mli
diff --git a/lib/hashset.ml b/clib/hashset.ml
index 7f96627a6..7f96627a6 100644
--- a/lib/hashset.ml
+++ b/clib/hashset.ml
diff --git a/lib/hashset.mli b/clib/hashset.mli
index ec79205a5..ec79205a5 100644
--- a/lib/hashset.mli
+++ b/clib/hashset.mli
diff --git a/lib/heap.ml b/clib/heap.ml
index a6109972d..a6109972d 100644
--- a/lib/heap.ml
+++ b/clib/heap.ml
diff --git a/lib/heap.mli b/clib/heap.mli
index 93d504c5a..93d504c5a 100644
--- a/lib/heap.mli
+++ b/clib/heap.mli
diff --git a/lib/iStream.ml b/clib/iStream.ml
index d3a54332a..d3a54332a 100644
--- a/lib/iStream.ml
+++ b/clib/iStream.ml
diff --git a/lib/iStream.mli b/clib/iStream.mli
index cd7940e8d..cd7940e8d 100644
--- a/lib/iStream.mli
+++ b/clib/iStream.mli
diff --git a/lib/int.ml b/clib/int.ml
index 63f62154d..63f62154d 100644
--- a/lib/int.ml
+++ b/clib/int.ml
diff --git a/lib/int.mli b/clib/int.mli
index b65367f7d..b65367f7d 100644
--- a/lib/int.mli
+++ b/clib/int.mli
diff --git a/lib/minisys.ml b/clib/minisys.ml
index 389b18ad4..389b18ad4 100644
--- a/lib/minisys.ml
+++ b/clib/minisys.ml
diff --git a/lib/monad.ml b/clib/monad.ml
index 2e55e9698..2e55e9698 100644
--- a/lib/monad.ml
+++ b/clib/monad.ml
diff --git a/lib/monad.mli b/clib/monad.mli
index 7b0a3e600..7b0a3e600 100644
--- a/lib/monad.mli
+++ b/clib/monad.mli
diff --git a/lib/option.ml b/clib/option.ml
index 98b168035..98b168035 100644
--- a/lib/option.ml
+++ b/clib/option.ml
diff --git a/lib/option.mli b/clib/option.mli
index 66f05023f..66f05023f 100644
--- a/lib/option.mli
+++ b/clib/option.mli
diff --git a/lib/predicate.ml b/clib/predicate.ml
index 1aa7db6af..1aa7db6af 100644
--- a/lib/predicate.ml
+++ b/clib/predicate.ml
diff --git a/lib/predicate.mli b/clib/predicate.mli
index cee3b0bd3..cee3b0bd3 100644
--- a/lib/predicate.mli
+++ b/clib/predicate.mli
diff --git a/lib/segmenttree.ml b/clib/segmenttree.ml
index d0ded4cb5..d0ded4cb5 100644
--- a/lib/segmenttree.ml
+++ b/clib/segmenttree.ml
diff --git a/lib/segmenttree.mli b/clib/segmenttree.mli
index e274a6fdc..e274a6fdc 100644
--- a/lib/segmenttree.mli
+++ b/clib/segmenttree.mli
diff --git a/lib/store.ml b/clib/store.ml
index 97a8fea08..97a8fea08 100644
--- a/lib/store.ml
+++ b/clib/store.ml
diff --git a/lib/store.mli b/clib/store.mli
index 5cc5bb859..5cc5bb859 100644
--- a/lib/store.mli
+++ b/clib/store.mli
diff --git a/lib/terminal.ml b/clib/terminal.ml
index 34efddfbc..34efddfbc 100644
--- a/lib/terminal.ml
+++ b/clib/terminal.ml
diff --git a/lib/terminal.mli b/clib/terminal.mli
index b1b76e6e2..b1b76e6e2 100644
--- a/lib/terminal.mli
+++ b/clib/terminal.mli
diff --git a/lib/trie.ml b/clib/trie.ml
index 0b0ba2761..0b0ba2761 100644
--- a/lib/trie.ml
+++ b/clib/trie.ml
diff --git a/lib/trie.mli b/clib/trie.mli
index a87acc8a6..a87acc8a6 100644
--- a/lib/trie.mli
+++ b/clib/trie.mli
diff --git a/lib/unicode.ml b/clib/unicode.ml
index f193c4e0f..f193c4e0f 100644
--- a/lib/unicode.ml
+++ b/clib/unicode.ml
diff --git a/lib/unicode.mli b/clib/unicode.mli
index 32ffbb8e9..32ffbb8e9 100644
--- a/lib/unicode.mli
+++ b/clib/unicode.mli
diff --git a/lib/unicodetable.ml b/clib/unicodetable.ml
index b607058c6..b607058c6 100644
--- a/lib/unicodetable.ml
+++ b/clib/unicodetable.ml
diff --git a/lib/unionfind.ml b/clib/unionfind.ml
index f9c92d6a8..f9c92d6a8 100644
--- a/lib/unionfind.ml
+++ b/clib/unionfind.ml
diff --git a/lib/unionfind.mli b/clib/unionfind.mli
index b242232ed..b242232ed 100644
--- a/lib/unionfind.mli
+++ b/clib/unionfind.mli
diff --git a/configure.ml b/configure.ml
index 06aa5e766..0698d93e2 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1143,7 +1143,7 @@ let write_configml f =
                                     core_src_dirs in
 
   pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
-  pr "\nlet api_dirs = [\"API\"; \"lib\"]\n";
+  pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n";
   pr "\nlet plugins_dirs = [\n";
 
   let plugins = Sys.readdir "plugins" in
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 66f939a91..b2260ba09 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