From 8ace437982f1b806895bb136cf009679ff9ca80c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Jan 2006 18:33:12 +0000
Subject: Ajout printer Idset.t

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index cd837ab6a6..30a6ed96d9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,6 +18,7 @@
 #use "vm_printers.ml";;
 
 #install_printer  (* identifier *) ppid;;
+#install_printer  (* identifier *) ppidset;;
 #install_printer  (* label *) pplab;;
 #install_printer  (* mod_self_id *) ppmsid;;
 #install_printer  (* mod_bound_id *) ppmbid;;
-- 
cgit v1.2.3