diff options
| author | Enrico | 2016-03-03 22:06:49 +0100 |
|---|---|---|
| committer | Enrico | 2016-03-03 22:06:49 +0100 |
| commit | 696a53e13cf0aa46b72f1f2d47c7f619e825ec02 (patch) | |
| tree | 8fbafaafec6783164b6e1b3b07a467a22b538e0a /mathcomp | |
| parent | 42ae48695694641c67a86adb299e34f6c1366f4f (diff) | |
| parent | a8962654c562349f24728613352ea76268227471 (diff) | |
Merge pull request #33 from ejgallego/search-print-with-msg
[search] Use msg_info to notify search results.
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) ] -> |