From 4e6d36c5977a874dc5adcdfb041c0a40c340e0b7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Dec 2014 11:20:04 +0100
Subject: More printers in tracer.

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

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 7f72f55d9d..b2eb280d6c 100644
--- a/dev/include
+++ b/dev/include
@@ -52,6 +52,8 @@
 #install_printer  (* 'a scheme_kind *) ppscheme;;
 #install_printer  (* type_judgement *) pptype;;
 #install_printer  (* judgement *) ppj;;
+#install_printer  (* id set *) ppidset;;
+#install_printer  (* int set *) ppintset;;
 
 #install_printer  (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
 #install_printer  (* Reductionops machine stack *) pp_stack_t;;
-- 
cgit v1.2.3