diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-16 10:58:52 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-22 16:36:32 +0100 |
commit | 87cbd64254f33439882156d9a297a6a2f6886057 (patch) | |
tree | 8ffc7a81a0018c0a7d91c24871c84da00bea4996 /dev/db | |
parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) |
Cleanup debug printers a bit, add generated mli.
Diffstat (limited to 'dev/db')
-rw-r--r-- | dev/db | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -42,7 +42,6 @@ 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 install_printer Top_printers.ppnamedcontextval @@ -59,8 +58,8 @@ install_printer Top_printers.pphintdb install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc -install_printer Top_printers.prsubst -install_printer Top_printers.prdelta +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta install_printer Top_printers.ppfconstr install_printer Top_printers.ppgenarginfo install_printer Top_printers.ppgenargargt |