Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.

7 files changed, 128 insertions, 122 deletions

diff --git a/dev/base_db b/dev/base_db
index e18ac534ac..155e9591e0 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -1,4 +1,5 @@
 source core.dbg
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 install_printer Top_printers.ppid
 install_printer Top_printers.ppsp
diff --git a/dev/checker.dbg b/dev/checker.dbg
index b2323b6175..b5b7f0e6d3 100644
--- a/dev/checker.dbg
+++ b/dev/checker.dbg
@@ -2,5 +2,6 @@ load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
 load_printer dynlink.cma
+load_printer config.cma
 load_printer lib.cma
 load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
index 327e636c57..fcb6f679ed 100644
--- a/dev/checker_db
+++ b/dev/checker_db
@@ -2,38 +2,4 @@ source checker.dbg
 
 load_printer checker_printers.cmo
 
-install_printer Checker_printers.pP
-
-install_printer Checker_printers.ppfuture
-
-install_printer Checker_printers.ppid
-install_printer Checker_printers.pplab
-install_printer Checker_printers.ppmbid
-install_printer Checker_printers.ppdir
-install_printer Checker_printers.ppmp
-install_printer Checker_printers.ppcon
-install_printer Checker_printers.ppproj
-install_printer Checker_printers.ppkn
-install_printer Checker_printers.ppmind
-install_printer Checker_printers.ppind
-
-install_printer Checker_printers.ppbigint
-
-install_printer Checker_printers.ppintset
-install_printer Checker_printers.ppidset
-
-install_printer Checker_printers.ppidmapgen
-
-install_printer Checker_printers.ppididmap
-
-install_printer Checker_printers.ppuni
-install_printer Checker_printers.ppuni_level
-install_printer Checker_printers.ppuniverse_set
-install_printer Checker_printers.ppuniverse_instance
-install_printer Checker_printers.ppauniverse_context
-install_printer Checker_printers.ppuniverse_context
-install_printer Checker_printers.ppconstraints
-install_printer Checker_printers.ppuniverse_context_future
-install_printer Checker_printers.ppuniverses
-
-install_printer Checker_printers.pploc
+source checker_printers.dbg
diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg
new file mode 100644
index 0000000000..9ebbd74834
--- /dev/null
+++ b/dev/checker_printers.dbg
@@ -0,0 +1,35 @@
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
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
diff --git a/dev/db b/dev/db
index 2f8c13485a..8733c684af 100644
--- a/dev/db
+++ b/dev/db
@@ -1,88 +1,6 @@
 source core.dbg
+
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 
-install_printer Top_printers.pP
-install_printer Top_printers.ppfuture
-install_printer Top_printers.ppid
-install_printer Top_printers.pplab
-install_printer Top_printers.ppmbid
-install_printer Top_printers.ppdir
-install_printer Top_printers.ppmp
-install_printer Top_printers.ppcon
-install_printer Top_printers.ppproj
-install_printer Top_printers.ppkn
-install_printer Top_printers.ppmind
-install_printer Top_printers.ppind
-install_printer Top_printers.ppsp
-install_printer Top_printers.ppqualid
-install_printer Top_printers.ppclindex
-install_printer Top_printers.ppscheme
-install_printer Top_printers.ppwf_paths
-install_printer Top_printers.ppevar
-install_printer Top_printers.ppconstr
-install_printer Top_printers.ppsconstr
-install_printer Top_printers.ppeconstr
-install_printer Top_printers.ppconstr_expr
-install_printer Top_printers.ppglob_constr
-install_printer Top_printers.pppattern
-install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
-install_printer Top_printers.ppintset
-install_printer Top_printers.ppidset
-install_printer Top_printers.ppidmapgen
-install_printer Top_printers.ppididmap
-install_printer Top_printers.ppconstrunderbindersidmap
-install_printer Top_printers.ppevarsubst
-install_printer Top_printers.ppunbound_ltac_var_map
-install_printer Top_printers.ppclosure
-install_printer Top_printers.ppclosedglobconstr
-install_printer Top_printers.ppclosedglobconstridmap
-install_printer Top_printers.ppglobal
-install_printer Top_printers.ppconst
-install_printer Top_printers.ppvar
-install_printer Top_printers.ppj
-install_printer Top_printers.ppsubst
-install_printer Top_printers.ppdelta
-install_printer Top_printers.pp_idpred
-install_printer Top_printers.pp_cpred
-install_printer Top_printers.pp_transparent_state
-install_printer Top_printers.pp_stack_t
-install_printer Top_printers.pp_cst_stack_t
-install_printer Top_printers.pp_state_t
-install_printer Top_printers.ppmetas
-install_printer Top_printers.ppevm
-install_printer Top_printers.ppexistentialset
-install_printer Top_printers.ppexistentialfilter
-install_printer Top_printers.ppclenv
-install_printer Top_printers.ppgoalgoal
-install_printer Top_printers.ppgoal
-install_printer Top_printers.pphintdb
-install_printer Top_printers.ppproofview
-install_printer Top_printers.ppopenconstr
-install_printer Top_printers.pproof
-install_printer Top_printers.ppuni
-install_printer Top_printers.ppuni_level
-install_printer Top_printers.ppuniverse_set
-install_printer Top_printers.ppuniverse_instance
-install_printer Top_printers.ppuniverse_context
-install_printer Top_printers.ppuniverse_context_set
-install_printer Top_printers.ppuniverse_subst
-install_printer Top_printers.ppuniverse_opt_subst
-install_printer Top_printers.ppuniverse_level_subst
-install_printer Top_printers.ppevar_universe_context
-install_printer Top_printers.ppconstraints
-install_printer Top_printers.ppuniverseconstraints
-install_printer Top_printers.ppuniverse_context_future
-install_printer Top_printers.ppcumulativity_info
-install_printer Top_printers.ppabstract_cumulativity_info
-install_printer Top_printers.ppuniverses
-install_printer Top_printers.ppnamedcontextval
-install_printer Top_printers.ppenv
-install_printer Top_printers.pptac
-install_printer Top_printers.ppobj
-install_printer Top_printers.pploc
-install_printer Top_printers.pp_argument_type
-install_printer Top_printers.pp_generic_argument
-install_printer Top_printers.ppgenarginfo
-install_printer Top_printers.ppgenargargt
-install_printer Top_printers.ppist
+source top_printers.dbg
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
new file mode 100644
index 0000000000..eab88c7290
--- /dev/null
+++ b/dev/top_printers.dbg
@@ -0,0 +1,85 @@
+install_printer Top_printers.pP
+install_printer Top_printers.ppfuture
+install_printer Top_printers.ppid
+install_printer Top_printers.pplab
+install_printer Top_printers.ppmbid
+install_printer Top_printers.ppdir
+install_printer Top_printers.ppmp
+install_printer Top_printers.ppcon
+install_printer Top_printers.ppproj
+install_printer Top_printers.ppkn
+install_printer Top_printers.ppmind
+install_printer Top_printers.ppind
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
+install_printer Top_printers.ppscheme
+install_printer Top_printers.ppwf_paths
+install_printer Top_printers.ppevar
+install_printer Top_printers.ppconstr
+install_printer Top_printers.ppsconstr
+install_printer Top_printers.ppeconstr
+install_printer Top_printers.ppconstr_expr
+install_printer Top_printers.ppglob_constr
+install_printer Top_printers.pppattern
+install_printer Top_printers.ppfconstr
+install_printer Top_printers.ppbigint
+install_printer Top_printers.ppintset
+install_printer Top_printers.ppidset
+install_printer Top_printers.ppidmapgen
+install_printer Top_printers.ppididmap
+install_printer Top_printers.ppconstrunderbindersidmap
+install_printer Top_printers.ppevarsubst
+install_printer Top_printers.ppunbound_ltac_var_map
+install_printer Top_printers.ppclosure
+install_printer Top_printers.ppclosedglobconstr
+install_printer Top_printers.ppclosedglobconstridmap
+install_printer Top_printers.ppglobal
+install_printer Top_printers.ppconst
+install_printer Top_printers.ppvar
+install_printer Top_printers.ppj
+install_printer Top_printers.ppsubst
+install_printer Top_printers.ppdelta
+install_printer Top_printers.pp_idpred
+install_printer Top_printers.pp_cpred
+install_printer Top_printers.pp_transparent_state
+install_printer Top_printers.pp_stack_t
+install_printer Top_printers.pp_cst_stack_t
+install_printer Top_printers.pp_state_t
+install_printer Top_printers.ppmetas
+install_printer Top_printers.ppevm
+install_printer Top_printers.ppexistentialset
+install_printer Top_printers.ppexistentialfilter
+install_printer Top_printers.ppclenv
+install_printer Top_printers.ppgoalgoal
+install_printer Top_printers.ppgoal
+install_printer Top_printers.pphintdb
+install_printer Top_printers.ppproofview
+install_printer Top_printers.ppopenconstr
+install_printer Top_printers.pproof
+install_printer Top_printers.ppuni
+install_printer Top_printers.ppuni_level
+install_printer Top_printers.ppuniverse_set
+install_printer Top_printers.ppuniverse_instance
+install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppuniverse_context_set
+install_printer Top_printers.ppuniverse_subst
+install_printer Top_printers.ppuniverse_opt_subst
+install_printer Top_printers.ppuniverse_level_subst
+install_printer Top_printers.ppevar_universe_context
+install_printer Top_printers.ppconstraints
+install_printer Top_printers.ppuniverseconstraints
+install_printer Top_printers.ppuniverse_context_future
+install_printer Top_printers.ppcumulativity_info
+install_printer Top_printers.ppabstract_cumulativity_info
+install_printer Top_printers.ppuniverses
+install_printer Top_printers.ppnamedcontextval
+install_printer Top_printers.ppenv
+install_printer Top_printers.pptac
+install_printer Top_printers.ppobj
+install_printer Top_printers.pploc
+install_printer Top_printers.pp_argument_type
+install_printer Top_printers.pp_generic_argument
+install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppgenargargt
+install_printer Top_printers.ppist