[search] [ssr] Emit deprecated message when calling search from ssreflect

but ssrsearch is not loaded.

Fixes #12338

3 files changed, 35 insertions, 0 deletions

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 7ef3e44848..24772a8514 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -300,6 +300,35 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
           Ssrview.AdaptorDb.declare k hints }
 END
 
+(** Search compatibility *)
+
+{
+
+  let warn_search_moved_enabled = ref true
+  let warn_search_moved = CWarnings.create ~name:"ssr-search-moved"
+      ~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"))
+
+open G_vernac
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: query_command;
+
+  query_command:
+    [ [ IDENT "Search"; s = search_query; l = search_queries; "." ->
+          { let (sl,m) = l in
+            if !warn_search_moved_enabled then warn_search_moved ();
+            fun g ->
+              Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) }
+      ] ]
+;
+END
+
 (** Keyword compatibility fixes. *)
 
 (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli
index 327a2d4660..93339313f0 100644
--- a/plugins/ssr/ssrvernac.mli
+++ b/plugins/ssr/ssrvernac.mli
@@ -9,3 +9,5 @@
 (************************************************************************)
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+
+val warn_search_moved_enabled : bool ref
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 1651e1cc71..6d68cc13ab 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -299,6 +299,10 @@ let ssrdisplaysearch gr env t =
   let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
   Feedback.msg_notice (hov 2 pr_res ++ fnl ())
 
+(* Remove the warning entirely when this plugin is loaded. *)
+let _ =
+  Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false
+
 let deprecated_search =
   CWarnings.create
     ~name:"deprecated-ssr-search"