From 5eff644c658d1765ba73cd9e73c5bd7819c7d644 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Oct 2014 16:04:15 +0200
Subject: Adding printer for named_context_val and Goal.goal in debugger.

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

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index ac09150075..069622a028 100644
--- a/dev/include
+++ b/dev/include
@@ -69,6 +69,7 @@
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 #install_printer  (* Hint_db.t *) pphintdb;;
+#install_printer  (* named_context_val *) ppnamedcontextval;;
 
 #install_printer  (* tactic *) pptac;;
 #install_printer  (* object *) ppobj;;
-- 
cgit v1.2.3