[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 21555f5e5d..d60f5037bb 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 d31b60cd02..75cec8f0cf 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 2f7ce6ef35..33ab72e689 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 7e0f588759..5b5855782f 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 f436d3e8f1..7e8f3e3e74 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 7d809f67a5..08829b5544 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 be9f40c1fb..be9f40c1fb 100644
--- a/lib/backtrace.ml
+++ b/clib/backtrace.ml
diff --git a/lib/backtrace.mli b/clib/backtrace.mli
index dd82165b6d..dd82165b6d 100644
--- a/lib/backtrace.mli
+++ b/clib/backtrace.mli
diff --git a/lib/bigint.ml b/clib/bigint.ml
index 4f8b95d592..4f8b95d592 100644
--- a/lib/bigint.ml
+++ b/clib/bigint.ml
diff --git a/lib/bigint.mli b/clib/bigint.mli
index 2a5a5f122d..2a5a5f122d 100644
--- a/lib/bigint.mli
+++ b/clib/bigint.mli
diff --git a/lib/cArray.ml b/clib/cArray.ml
index 013585735c..013585735c 100644
--- a/lib/cArray.ml
+++ b/clib/cArray.ml
diff --git a/lib/cArray.mli b/clib/cArray.mli
index 325ff8edcc..325ff8edcc 100644
--- a/lib/cArray.mli
+++ b/clib/cArray.mli
diff --git a/lib/cEphemeron.ml b/clib/cEphemeron.ml
index 8b253a7901..8b253a7901 100644
--- a/lib/cEphemeron.ml
+++ b/clib/cEphemeron.ml
diff --git a/lib/cEphemeron.mli b/clib/cEphemeron.mli
index d8a1f27573..d8a1f27573 100644
--- a/lib/cEphemeron.mli
+++ b/clib/cEphemeron.mli
diff --git a/lib/cList.ml b/clib/cList.ml
index 0ef7c3d8ba..0ef7c3d8ba 100644
--- a/lib/cList.ml
+++ b/clib/cList.ml
diff --git a/lib/cList.mli b/clib/cList.mli
index f87db04cf4..f87db04cf4 100644
--- a/lib/cList.mli
+++ b/clib/cList.mli
diff --git a/lib/cMap.ml b/clib/cMap.ml
index b4c4aedd0e..b4c4aedd0e 100644
--- a/lib/cMap.ml
+++ b/clib/cMap.ml
diff --git a/lib/cMap.mli b/clib/cMap.mli
index 5e65bd200a..5e65bd200a 100644
--- a/lib/cMap.mli
+++ b/clib/cMap.mli
diff --git a/lib/cObj.ml b/clib/cObj.ml
index 7f3ee18553..7f3ee18553 100644
--- a/lib/cObj.ml
+++ b/clib/cObj.ml
diff --git a/lib/cObj.mli b/clib/cObj.mli
index 16933a4aa4..16933a4aa4 100644
--- a/lib/cObj.mli
+++ b/clib/cObj.mli
diff --git a/lib/cSet.ml b/clib/cSet.ml
index ed65edf16e..ed65edf16e 100644
--- a/lib/cSet.ml
+++ b/clib/cSet.ml
diff --git a/lib/cSet.mli b/clib/cSet.mli
index 2eb9bce869..2eb9bce869 100644
--- a/lib/cSet.mli
+++ b/clib/cSet.mli
diff --git a/lib/cSig.mli b/clib/cSig.mli
index 32e9d2af0c..32e9d2af0c 100644
--- a/lib/cSig.mli
+++ b/clib/cSig.mli
diff --git a/lib/cStack.ml b/clib/cStack.ml
index 4acb2930c5..4acb2930c5 100644
--- a/lib/cStack.ml
+++ b/clib/cStack.ml
diff --git a/lib/cStack.mli b/clib/cStack.mli
index 8dde1d1a1a..8dde1d1a1a 100644
--- a/lib/cStack.mli
+++ b/clib/cStack.mli
diff --git a/lib/cString.ml b/clib/cString.ml
index f2242460e8..f2242460e8 100644
--- a/lib/cString.ml
+++ b/clib/cString.ml
diff --git a/lib/cString.mli b/clib/cString.mli
index 29d3a44995..29d3a44995 100644
--- a/lib/cString.mli
+++ b/clib/cString.mli
diff --git a/lib/cThread.ml b/clib/cThread.ml
index 0221e690e8..0221e690e8 100644
--- a/lib/cThread.ml
+++ b/clib/cThread.ml
diff --git a/lib/cThread.mli b/clib/cThread.mli
index 66f039bb52..66f039bb52 100644
--- a/lib/cThread.mli
+++ b/clib/cThread.mli
diff --git a/lib/cUnix.ml b/clib/cUnix.ml
index 34fb660db4..34fb660db4 100644
--- a/lib/cUnix.ml
+++ b/clib/cUnix.ml
diff --git a/lib/cUnix.mli b/clib/cUnix.mli
index d08dc4c403..d08dc4c403 100644
--- a/lib/cUnix.mli
+++ b/clib/cUnix.mli
diff --git a/lib/canary.ml b/clib/canary.ml
index 0ed1d28f37..0ed1d28f37 100644
--- a/lib/canary.ml
+++ b/clib/canary.ml
diff --git a/lib/canary.mli b/clib/canary.mli
index 904b88213c..904b88213c 100644
--- a/lib/canary.mli
+++ b/clib/canary.mli
diff --git a/lib/clib.mllib b/clib/clib.mllib
index 5c1f7d9af8..bd5ddb1525 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 373269b4f5..373269b4f5 100644
--- a/lib/deque.ml
+++ b/clib/deque.ml
diff --git a/lib/deque.mli b/clib/deque.mli
index 23cb1e4919..23cb1e4919 100644
--- a/lib/deque.mli
+++ b/clib/deque.mli
diff --git a/lib/dyn.ml b/clib/dyn.ml
index 64535d35f6..64535d35f6 100644
--- a/lib/dyn.ml
+++ b/clib/dyn.ml
diff --git a/lib/dyn.mli b/clib/dyn.mli
index 2206394e2d..2206394e2d 100644
--- a/lib/dyn.mli
+++ b/clib/dyn.mli
diff --git a/lib/exninfo.ml b/clib/exninfo.ml
index 167d3d6dc8..167d3d6dc8 100644
--- a/lib/exninfo.ml
+++ b/clib/exninfo.ml
diff --git a/lib/exninfo.mli b/clib/exninfo.mli
index c960ac7c08..c960ac7c08 100644
--- a/lib/exninfo.mli
+++ b/clib/exninfo.mli
diff --git a/lib/hMap.ml b/clib/hMap.ml
index 37079af783..37079af783 100644
--- a/lib/hMap.ml
+++ b/clib/hMap.ml
diff --git a/lib/hMap.mli b/clib/hMap.mli
index c77bfced88..c77bfced88 100644
--- a/lib/hMap.mli
+++ b/clib/hMap.mli
diff --git a/lib/hashcons.ml b/clib/hashcons.ml
index ee22325811..ee22325811 100644
--- a/lib/hashcons.ml
+++ b/clib/hashcons.ml
diff --git a/lib/hashcons.mli b/clib/hashcons.mli
index fbd2ebcf9a..fbd2ebcf9a 100644
--- a/lib/hashcons.mli
+++ b/clib/hashcons.mli
diff --git a/lib/hashset.ml b/clib/hashset.ml
index 7f96627a68..7f96627a68 100644
--- a/lib/hashset.ml
+++ b/clib/hashset.ml
diff --git a/lib/hashset.mli b/clib/hashset.mli
index ec79205a5c..ec79205a5c 100644
--- a/lib/hashset.mli
+++ b/clib/hashset.mli
diff --git a/lib/heap.ml b/clib/heap.ml
index a6109972d7..a6109972d7 100644
--- a/lib/heap.ml
+++ b/clib/heap.ml
diff --git a/lib/heap.mli b/clib/heap.mli
index 93d504c5ac..93d504c5ac 100644
--- a/lib/heap.mli
+++ b/clib/heap.mli
diff --git a/lib/iStream.ml b/clib/iStream.ml
index d3a54332a1..d3a54332a1 100644
--- a/lib/iStream.ml
+++ b/clib/iStream.ml
diff --git a/lib/iStream.mli b/clib/iStream.mli
index cd7940e8d3..cd7940e8d3 100644
--- a/lib/iStream.mli
+++ b/clib/iStream.mli
diff --git a/lib/int.ml b/clib/int.ml
index 63f62154d8..63f62154d8 100644
--- a/lib/int.ml
+++ b/clib/int.ml
diff --git a/lib/int.mli b/clib/int.mli
index b65367f7d4..b65367f7d4 100644
--- a/lib/int.mli
+++ b/clib/int.mli
diff --git a/lib/minisys.ml b/clib/minisys.ml
index 389b18ad4e..389b18ad4e 100644
--- a/lib/minisys.ml
+++ b/clib/minisys.ml
diff --git a/lib/monad.ml b/clib/monad.ml
index 2e55e9698c..2e55e9698c 100644
--- a/lib/monad.ml
+++ b/clib/monad.ml
diff --git a/lib/monad.mli b/clib/monad.mli
index 7b0a3e600f..7b0a3e600f 100644
--- a/lib/monad.mli
+++ b/clib/monad.mli
diff --git a/lib/option.ml b/clib/option.ml
index 98b1680354..98b1680354 100644
--- a/lib/option.ml
+++ b/clib/option.ml
diff --git a/lib/option.mli b/clib/option.mli
index 66f05023f7..66f05023f7 100644
--- a/lib/option.mli
+++ b/clib/option.mli
diff --git a/lib/predicate.ml b/clib/predicate.ml
index 1aa7db6af1..1aa7db6af1 100644
--- a/lib/predicate.ml
+++ b/clib/predicate.ml
diff --git a/lib/predicate.mli b/clib/predicate.mli
index cee3b0bd39..cee3b0bd39 100644
--- a/lib/predicate.mli
+++ b/clib/predicate.mli
diff --git a/lib/segmenttree.ml b/clib/segmenttree.ml
index d0ded4cb59..d0ded4cb59 100644
--- a/lib/segmenttree.ml
+++ b/clib/segmenttree.ml
diff --git a/lib/segmenttree.mli b/clib/segmenttree.mli
index e274a6fdc8..e274a6fdc8 100644
--- a/lib/segmenttree.mli
+++ b/clib/segmenttree.mli
diff --git a/lib/store.ml b/clib/store.ml
index 97a8fea085..97a8fea085 100644
--- a/lib/store.ml
+++ b/clib/store.ml
diff --git a/lib/store.mli b/clib/store.mli
index 5cc5bb8593..5cc5bb8593 100644
--- a/lib/store.mli
+++ b/clib/store.mli
diff --git a/lib/terminal.ml b/clib/terminal.ml
index 34efddfbca..34efddfbca 100644
--- a/lib/terminal.ml
+++ b/clib/terminal.ml
diff --git a/lib/terminal.mli b/clib/terminal.mli
index b1b76e6e2a..b1b76e6e2a 100644
--- a/lib/terminal.mli
+++ b/clib/terminal.mli
diff --git a/lib/trie.ml b/clib/trie.ml
index 0b0ba27613..0b0ba27613 100644
--- a/lib/trie.ml
+++ b/clib/trie.ml
diff --git a/lib/trie.mli b/clib/trie.mli
index a87acc8a69..a87acc8a69 100644
--- a/lib/trie.mli
+++ b/clib/trie.mli
diff --git a/lib/unicode.ml b/clib/unicode.ml
index f193c4e0f8..f193c4e0f8 100644
--- a/lib/unicode.ml
+++ b/clib/unicode.ml
diff --git a/lib/unicode.mli b/clib/unicode.mli
index 32ffbb8e94..32ffbb8e94 100644
--- a/lib/unicode.mli
+++ b/clib/unicode.mli
diff --git a/lib/unicodetable.ml b/clib/unicodetable.ml
index b607058c64..b607058c64 100644
--- a/lib/unicodetable.ml
+++ b/clib/unicodetable.ml
diff --git a/lib/unionfind.ml b/clib/unionfind.ml
index f9c92d6a8e..f9c92d6a8e 100644
--- a/lib/unionfind.ml
+++ b/clib/unionfind.ml
diff --git a/lib/unionfind.mli b/clib/unionfind.mli
index b242232edb..b242232edb 100644
--- a/lib/unionfind.mli
+++ b/clib/unionfind.mli
diff --git a/configure.ml b/configure.ml
index 06aa5e7666..0698d93e26 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 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