From a82f73d1fec1f200904819cf18dec75780c3a505 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Oct 2014 17:22:17 +0200
Subject: Adding a printer for hints.

---
 dev/include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 941fa3383b..ac09150075 100644
--- a/dev/include
+++ b/dev/include
@@ -68,6 +68,7 @@
 #install_printer  (* Evar.Set.t *) ppexistentialset;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
+#install_printer  (* Hint_db.t *) pphintdb;;
 
 #install_printer  (* tactic *) pptac;;
 #install_printer  (* object *) ppobj;;
-- 
cgit v1.2.3