From 57c023fe6b5c7f97403d849f7ca618c98d1af1a4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 17 May 2020 13:45:06 +0200
Subject: [search] [ssr] Emit deprecated message when calling search from
 ssreflect

but ssrsearch is not loaded.

Fixes #12338
---
 plugins/ssrsearch/g_search.mlg | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/ssrsearch')

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"
-- 
cgit v1.2.3