diff options
| author | Pierre-Marie Pédrot | 2017-07-14 14:10:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-14 14:10:30 +0200 |
| commit | 75bc9715c48f7b4f983d22cab27ce890d5d500a4 (patch) | |
| tree | 60e4199867e630069985997bccd8f4446801b04f /dev | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Adding debug printers related to universes in the default debugger source file.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 10 |
1 files changed, 10 insertions, 0 deletions
@@ -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 |