From 87cbd64254f33439882156d9a297a6a2f6886057 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 16 Dec 2017 10:58:52 +0100
Subject: Cleanup debug printers a bit, add generated mli.

---
 dev/db | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'dev/db')

diff --git a/dev/db b/dev/db
index 24ae3957ef..f716450413 100644
--- a/dev/db
+++ b/dev/db
@@ -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
-- 
cgit v1.2.3