diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 176a6c333..b3694d0e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -208,7 +208,7 @@ let display_cmd_header loc com = let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str (" ["^cmd^"] ")); + str " [" ++ str cmd ++ str "] "); Pp.flush_all () let rec vernac_com verbosely checknav (loc,com) = |