From 05adb6e2574fa4851f6dfbcc5aa7c73254049e5c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Thu, 25 Apr 2019 15:12:42 +0200
Subject: Add a typing colon in the output of the Search ssreflect vernacular

See also PR math-comp/math-comp#73
---
 plugins/ssr/ssrvernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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 ())
 
 }
-- 
cgit v1.2.3