Fixes a bug in Ppvernac which had braces and bullets printed with an ending

period.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15509 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 7 insertions, 5 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index efca60f00d..9513001f47 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -62,7 +62,11 @@ let pr_module = Libnames.pr_reference
 
 let pr_import_module = Libnames.pr_reference
 
-let sep_end () = str"."
+let sep_end = function
+  | VernacBullet _
+  | VernacSubproof None
+  | VernacEndSubproof -> str""
+  | _ -> str"."
 
 (* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
 
@@ -483,7 +487,7 @@ let rec pr_vernac = function
   (* Control *)
   | VernacList l ->
       hov 2 (str"[" ++ spc() ++
-             prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l
+             prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
              ++ spc() ++ str"]")
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
   ++ spc()) else spc()  ++ qs s
@@ -967,4 +971,4 @@ in pr_vernac
 
 let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
 
-let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end ()
+let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 992b5a7422..bea4993eda 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -20,8 +20,6 @@ open Libnames
 open Ppextend
 open Topconstr
 
-val sep_end : unit -> std_ppcmds
-
 (** Prints a vernac expression *)
 val pr_vernac_body : vernac_expr -> std_ppcmds