aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-14 14:10:30 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-14 14:10:30 +0200
commit75bc9715c48f7b4f983d22cab27ce890d5d500a4 (patch)
tree60e4199867e630069985997bccd8f4446801b04f /dev/db
parente3eb17a728d7b6874e67462e8a83fac436441872 (diff)
Adding debug printers related to universes in the default debugger source file.
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db10
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index 432baf8a6..a5518e3c4 100644
--- a/dev/db
+++ b/dev/db
@@ -32,6 +32,16 @@ install_printer Top_printers.ppeconstr
install_printer Top_printers.ppuni
install_printer Top_printers.ppuniverses
install_printer Top_printers.ppconstraints
+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.ppcumulativity_info
+install_printer Top_printers.ppabstract_cumulativity_info
install_printer Top_printers.pptype
install_printer Top_printers.ppj
install_printer Top_printers.ppenv