diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 0d2326f..d6a5175 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -1456,7 +1456,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in - msg (hov 2 pr_res ++ fnl ()) + msg_info (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index d76f761..c40d965 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -1437,7 +1437,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in - msg (hov 2 pr_res ++ fnl ()) + msg_info (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> |