diff options
| -rw-r--r-- | .merlin | 14 | ||||
| -rw-r--r-- | META.coq | 18 | ||||
| -rw-r--r-- | Makefile.build | 55 | ||||
| -rw-r--r-- | Makefile.checker | 2 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | clib/backtrace.ml (renamed from lib/backtrace.ml) | 0 | ||||
| -rw-r--r-- | clib/backtrace.mli (renamed from lib/backtrace.mli) | 0 | ||||
| -rw-r--r-- | clib/bigint.ml (renamed from lib/bigint.ml) | 0 | ||||
| -rw-r--r-- | clib/bigint.mli (renamed from lib/bigint.mli) | 0 | ||||
| -rw-r--r-- | clib/cArray.ml (renamed from lib/cArray.ml) | 0 | ||||
| -rw-r--r-- | clib/cArray.mli (renamed from lib/cArray.mli) | 0 | ||||
| -rw-r--r-- | clib/cEphemeron.ml (renamed from lib/cEphemeron.ml) | 0 | ||||
| -rw-r--r-- | clib/cEphemeron.mli (renamed from lib/cEphemeron.mli) | 0 | ||||
| -rw-r--r-- | clib/cList.ml (renamed from lib/cList.ml) | 0 | ||||
| -rw-r--r-- | clib/cList.mli (renamed from lib/cList.mli) | 0 | ||||
| -rw-r--r-- | clib/cMap.ml (renamed from lib/cMap.ml) | 0 | ||||
| -rw-r--r-- | clib/cMap.mli (renamed from lib/cMap.mli) | 0 | ||||
| -rw-r--r-- | clib/cObj.ml (renamed from lib/cObj.ml) | 0 | ||||
| -rw-r--r-- | clib/cObj.mli (renamed from lib/cObj.mli) | 0 | ||||
| -rw-r--r-- | clib/cSet.ml (renamed from lib/cSet.ml) | 0 | ||||
| -rw-r--r-- | clib/cSet.mli (renamed from lib/cSet.mli) | 0 | ||||
| -rw-r--r-- | clib/cSig.mli (renamed from lib/cSig.mli) | 0 | ||||
| -rw-r--r-- | clib/cStack.ml (renamed from lib/cStack.ml) | 0 | ||||
| -rw-r--r-- | clib/cStack.mli (renamed from lib/cStack.mli) | 0 | ||||
| -rw-r--r-- | clib/cString.ml (renamed from lib/cString.ml) | 0 | ||||
| -rw-r--r-- | clib/cString.mli (renamed from lib/cString.mli) | 0 | ||||
| -rw-r--r-- | clib/cThread.ml (renamed from lib/cThread.ml) | 0 | ||||
| -rw-r--r-- | clib/cThread.mli (renamed from lib/cThread.mli) | 0 | ||||
| -rw-r--r-- | clib/cUnix.ml (renamed from lib/cUnix.ml) | 0 | ||||
| -rw-r--r-- | clib/cUnix.mli (renamed from lib/cUnix.mli) | 0 | ||||
| -rw-r--r-- | clib/canary.ml (renamed from lib/canary.ml) | 0 | ||||
| -rw-r--r-- | clib/canary.mli (renamed from lib/canary.mli) | 0 | ||||
| -rw-r--r-- | clib/clib.mllib (renamed from lib/clib.mllib) | 49 | ||||
| -rw-r--r-- | clib/deque.ml (renamed from lib/deque.ml) | 0 | ||||
| -rw-r--r-- | clib/deque.mli (renamed from lib/deque.mli) | 0 | ||||
| -rw-r--r-- | clib/dyn.ml (renamed from lib/dyn.ml) | 0 | ||||
| -rw-r--r-- | clib/dyn.mli (renamed from lib/dyn.mli) | 0 | ||||
| -rw-r--r-- | clib/exninfo.ml (renamed from lib/exninfo.ml) | 0 | ||||
| -rw-r--r-- | clib/exninfo.mli (renamed from lib/exninfo.mli) | 0 | ||||
| -rw-r--r-- | clib/hMap.ml (renamed from lib/hMap.ml) | 0 | ||||
| -rw-r--r-- | clib/hMap.mli (renamed from lib/hMap.mli) | 0 | ||||
| -rw-r--r-- | clib/hashcons.ml (renamed from lib/hashcons.ml) | 0 | ||||
| -rw-r--r-- | clib/hashcons.mli (renamed from lib/hashcons.mli) | 0 | ||||
| -rw-r--r-- | clib/hashset.ml (renamed from lib/hashset.ml) | 0 | ||||
| -rw-r--r-- | clib/hashset.mli (renamed from lib/hashset.mli) | 0 | ||||
| -rw-r--r-- | clib/heap.ml (renamed from lib/heap.ml) | 0 | ||||
| -rw-r--r-- | clib/heap.mli (renamed from lib/heap.mli) | 0 | ||||
| -rw-r--r-- | clib/iStream.ml (renamed from lib/iStream.ml) | 0 | ||||
| -rw-r--r-- | clib/iStream.mli (renamed from lib/iStream.mli) | 0 | ||||
| -rw-r--r-- | clib/int.ml (renamed from lib/int.ml) | 0 | ||||
| -rw-r--r-- | clib/int.mli (renamed from lib/int.mli) | 0 | ||||
| -rw-r--r-- | clib/minisys.ml (renamed from lib/minisys.ml) | 0 | ||||
| -rw-r--r-- | clib/monad.ml (renamed from lib/monad.ml) | 0 | ||||
| -rw-r--r-- | clib/monad.mli (renamed from lib/monad.mli) | 0 | ||||
| -rw-r--r-- | clib/option.ml (renamed from lib/option.ml) | 0 | ||||
| -rw-r--r-- | clib/option.mli (renamed from lib/option.mli) | 0 | ||||
| -rw-r--r-- | clib/predicate.ml (renamed from lib/predicate.ml) | 0 | ||||
| -rw-r--r-- | clib/predicate.mli (renamed from lib/predicate.mli) | 0 | ||||
| -rw-r--r-- | clib/segmenttree.ml (renamed from lib/segmenttree.ml) | 0 | ||||
| -rw-r--r-- | clib/segmenttree.mli (renamed from lib/segmenttree.mli) | 0 | ||||
| -rw-r--r-- | clib/store.ml (renamed from lib/store.ml) | 0 | ||||
| -rw-r--r-- | clib/store.mli (renamed from lib/store.mli) | 0 | ||||
| -rw-r--r-- | clib/terminal.ml (renamed from lib/terminal.ml) | 0 | ||||
| -rw-r--r-- | clib/terminal.mli (renamed from lib/terminal.mli) | 0 | ||||
| -rw-r--r-- | clib/trie.ml (renamed from lib/trie.ml) | 0 | ||||
| -rw-r--r-- | clib/trie.mli (renamed from lib/trie.mli) | 0 | ||||
| -rw-r--r-- | clib/unicode.ml (renamed from lib/unicode.ml) | 0 | ||||
| -rw-r--r-- | clib/unicode.mli (renamed from lib/unicode.mli) | 0 | ||||
| -rw-r--r-- | clib/unicodetable.ml (renamed from lib/unicodetable.ml) | 0 | ||||
| -rw-r--r-- | clib/unionfind.ml (renamed from lib/unionfind.ml) | 0 | ||||
| -rw-r--r-- | clib/unionfind.mli (renamed from lib/unionfind.mli) | 0 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | lib/lib.mllib | 39 |
74 files changed, 102 insertions, 83 deletions
@@ -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 @@ -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 |