aboutsummaryrefslogtreecommitdiff
path: root/dev/core.dbg
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-17 15:24:15 +0200
committerEmilio Jesus Gallego Arias2018-10-23 00:42:04 +0200
commit1db19a8f454e0f8c5a60101c87ccd38e0883d530 (patch)
tree5b575feb0118a20aa027ebcce2b5028ccfd142cf /dev/core.dbg
parent2d714ebc0ea9588b4346249a574d9eda63dd389d (diff)
[build] Refactoring to config lib and ocamldebug tweaks.
We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile.
Diffstat (limited to 'dev/core.dbg')
-rw-r--r--dev/core.dbg4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/core.dbg b/dev/core.dbg
index 972ba701e4..f676b643e4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,6 +1,7 @@
-source camlp5.dbg
load_printer threads.cma
load_printer str.cma
+load_printer gramlib.cma
+load_printer config.cma
load_printer clib.cma
load_printer dynlink.cma
load_printer lib.cma
@@ -16,4 +17,3 @@ load_printer tactics.cma
load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
-load_printer ltac_plugin.cmo