aboutsummaryrefslogtreecommitdiff
path: root/dev/core.dbg
diff options
context:
space:
mode:
authorMaxime Dénès2017-03-24 16:15:32 +0100
committerMaxime Dénès2017-03-24 16:15:32 +0100
commitaf291869bb7d1184d8e655906572d75937ca829b (patch)
tree62a5ccf9ee7b115b7d1118cbc3db92c553261713 /dev/core.dbg
parent3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff)
parent7535e268f7706d1dee263fdbafadf920349103db (diff)
Merge branch 'trunk' into pr379
Diffstat (limited to 'dev/core.dbg')
-rw-r--r--dev/core.dbg3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/core.dbg b/dev/core.dbg
index 38b9b29463..f04e5c07b7 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -12,7 +12,8 @@ load_printer proofs.cma
load_printer parsing.cma
load_printer printing.cma
load_printer tactics.cma
+load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
load_printer highparsing.cma
-load_printer ltac.cma
+load_printer ltac_plugin.cmo