From 6251f1b0b453a90c1c2a993c6980c1f40bfb2de7 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 12 Mar 2020 11:08:57 +0100
Subject: Add message at the end of search results about implicit arguments

---
 vernac/vernacentries.ml | 5 +++--
 1 file 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
-- 
cgit v1.2.3