Bug et amliorations diverses

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

1 files changed, 2 insertions, 3 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b0b26b33c..b325c8b19 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -144,12 +144,11 @@ let rec vernac_com interpfun (loc,com) =
          | _ ->
 	     let fs = States.freeze () in
              if !translate_file then
-               msgnl
-		 (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end())
+               msgnl (pr_comments !comments ++ hov 0 (pr_vernac com))
              else
 	       (msgnl
                  (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         pr_vernac com ++ sep_end()));
+                         pr_vernac com));
 		 States.unfreeze fs));
        Constrintern.set_temporary_implicits_in [];
        Constrextern.set_temporary_implicits_out [];