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/include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 0d34595f4f..b982f4c9fa 100644
--- a/dev/include
+++ b/dev/include
@@ -36,7 +36,6 @@
 #install_printer  (* constraints *)  ppconstraints;;
 #install_printer  (* univ constraints *)  ppuniverseconstraints;;
 #install_printer  (* universe *)  ppuni;;
-#install_printer  (* universes *)  ppuniverse;;
 #install_printer  (* universes *)  ppuniverses;;
 #install_printer  (* univ level *) ppuni_level;;
 #install_printer  (* univ context *) ppuniverse_context;;
-- 
cgit v1.2.3