diff options
| author | Maxime Dénès | 2017-07-17 07:37:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-17 07:37:55 +0200 |
| commit | 15cdb11be5f6f452b54a2943897fadd99efd2ea7 (patch) | |
| tree | 0cfd5758f99db691e7b04b091575ece0c6639622 /dev | |
| parent | f7fda5a7e2b43e3ac24d0a2a5c5e4a7b9cda4bdd (diff) | |
| parent | 75bc9715c48f7b4f983d22cab27ce890d5d500a4 (diff) | |
Merge PR #879: Adding debug printers related to universes
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 |