From a2ce4da4c2b0dc81d4c61f3e672d6c9d65dba46b Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 22 Oct 2020 21:16:58 +0200
Subject: adjust Search deprecation warning

---
 plugins/ssr/ssrvernac.mlg | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 4a907b2795..91cd5b251c 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -309,9 +309,15 @@ END
       ~category:"deprecated" ~default:CWarnings.Enabled
       (fun () ->
          (Pp.strbrk
-            "SSReflect's Search command has been moved to the \
-             ssrsearch module; please Require that module if you \
-             still want to use SSReflect's Search command"))
+            "In previous versions of Coq, loading SSReflect had the effect of \
+             replacing the built-in 'Search' command with an SSReflect version \
+             of that command. \
+             Coq's own search feature was still available via 'SearchAbout' \
+             (but that alias is deprecated). \
+             This replacement no longer happens; now 'Search' calls Coq's own search \
+             feature even when SSReflect is loaded. \
+             If you want to use SSReflect's deprecated Search command \
+             instead of the built-in one, please Require the ssrsearch module."))
 
 open G_vernac
 }
-- 
cgit v1.2.3