diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 054b60853f..baaf8aa849 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -86,7 +86,13 @@ open Pputils let pr_module = Libnames.pr_qualid - let pr_import_module = Libnames.pr_qualid + let pr_one_import_filter_name (q,etc) = + Libnames.pr_qualid q ++ if etc then str "(..)" else mt() + + let pr_import_module (m,f) = + Libnames.pr_qualid m ++ match f with + | ImportAll -> mt() + | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns) let sep_end = function | VernacBullet _ |