diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 5 |
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 []; |