diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index bf7f082192..08f028465b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -465,7 +465,7 @@ let interp_modloc mr = (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in Feedback.msg_info (hov 2 pr_res ++ fnl ()) } |