aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-27 14:36:36 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-27 14:36:36 +0000
commit68b1fa3bceffef3c3dfef8b2f041f2e5eb4d3173 (patch)
treeaffda6fb63631bc55245a1f08bc4af41cbbdb3de /library
parentcaff708cff41f6bb91d26b59f3d93018f17f63ba (diff)
Improving formatting of output of "Test table".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/goptions.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index 858ebbfc8..550ded685 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -105,10 +105,10 @@ module MakeTable =
let print_table table_name printer table =
pp (str table_name ++
(hov 0
- (if MySet.is_empty table then str "None" ++ fnl ()
+ (if MySet.is_empty table then str " None" ++ fnl ()
else MySet.fold
- (fun a b -> printer a ++ spc () ++ b)
- table (mt ()) ++ fnl ())))
+ (fun a b -> spc () ++ printer a ++ b)
+ table (mt ()) ++ str "." ++ fnl ())))
class table_of_A () =
object