aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorherbelin2006-01-29 18:33:12 +0000
committerherbelin2006-01-29 18:33:12 +0000
commit8ace437982f1b806895bb136cf009679ff9ca80c (patch)
treec1886a79f3841b93e0e0e5453554afa91cdc3579 /dev/top_printers.ml
parent2ab4324677baa86bfd15716cae965f066bad7e53 (diff)
Ajout printer Idset.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f4f17c1d7a..1cd2369e64 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))