From 75bc9715c48f7b4f983d22cab27ce890d5d500a4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 14:10:30 +0200 Subject: Adding debug printers related to universes in the default debugger source file. --- dev/db | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'dev/db') 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 -- cgit v1.2.3