diff options
| author | Enrico Tassi | 2019-04-26 11:28:27 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-04-26 11:28:27 +0200 |
| commit | e518ed1ff4121cd5e5be0e970c88e19bf29552c2 (patch) | |
| tree | 4149c55216f17cf4e42682bf0e2f61b1b33cccab /plugins | |
| parent | 12e5d3cdef8b954fc3a7cdf1dfebc388bd546c3a (diff) | |
| parent | 05adb6e2574fa4851f6dfbcc5aa7c73254049e5c (diff) | |
Merge PR #10001: Add a typing colon in the output of the Search ssreflect vernacular
Reviewed-by: gares
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 ()) } |