diff options
| author | herbelin | 2006-01-29 18:33:12 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-29 18:33:12 +0000 |
| commit | 8ace437982f1b806895bb136cf009679ff9ca80c (patch) | |
| tree | c1886a79f3841b93e0e0e5453554afa91cdc3579 /dev/top_printers.ml | |
| parent | 2ab4324677baa86bfd15716cae965f066bad7e53 (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.ml | 5 |
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)) |
