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
HoTT · Jan 27, 2013 · 68b1fa3 · 68b1fa3
1 parent caff708
commit 68b1fa3
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
@@ -85,7 +85,7 @@ module PrintingCasesIf =
   PrintingInductiveMake (struct
     let encode = encode_bool
     let field = "If"
-    let title = "Types leading to pretty-printing of Cases using a `if' form: "
+    let title = "Types leading to pretty-printing of Cases using a `if' form:"
     let member_message s b =
       str "Cases on elements of " ++ s ++
       str