diff options
| author | SimonBoulier | 2020-03-12 11:08:57 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-03-12 11:22:50 +0100 |
| commit | 6251f1b0b453a90c1c2a993c6980c1f40bfb2de7 (patch) | |
| tree | f2db97f61da5d572dceedbef117272fd962b6f9e | |
| parent | 50ad4221263d1a3243541a1108e447ac3c1b3742 (diff) | |
Add message at the end of search results about implicit arguments
| -rw-r--r-- | vernac/vernacentries.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3e333db68e..14f6c7c3e7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1782,7 +1782,7 @@ let vernac_search ~pstate ~atts s gopt r = end in Feedback.msg_notice pp in - match s with + (match s with | SearchPattern c -> (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> @@ -1795,7 +1795,8 @@ let vernac_search ~pstate ~atts s gopt r = Search.prioritize_search) pr_search | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search + Search.prioritize_search) pr_search); + Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") let vernac_locate ~pstate = function | LocateAny {v=AN qid} -> print_located_qualid qid |