Ajout printer Idset.t

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 5 insertions, 2 deletions

diff --git a/dev/base_include b/dev/base_include
index cd837ab6a..30a6ed96d 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;;
diff --git a/dev/db b/dev/db
index 751043977..38463b413 100644
--- a/dev/db
+++ b/dev/db
@@ -2,6 +2,7 @@ load_printer "gramlib.cma"
 load_printer "printers.cma"
 
 install_printer Top_printers.ppid
+install_printer Top_printers.ppidset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppmsid
 install_printer Top_printers.ppmbid
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f4f17c1d7..1cd2369e6 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -9,6 +9,7 @@
 (* Printers for the ocaml toplevel. *)
 
 open System
+open Util
 open Pp
 open Names
 open Libnames
@@ -52,6 +53,8 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
 
+let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l))
+
 let pP s = pp (hov 0 s)
 
 let safe_pr_global = function 
@@ -83,8 +86,6 @@ let ppgoal g = pp(db_pr_goal g)
 let pr_gls gls =
   hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
 
-open Util
-
 let pr_glls glls =
   hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl db_pr_goal (sig_it glls))