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
---
 vernac/g_vernac.mlg | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index fe3bb9b890..45bf61d79e 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -35,6 +35,9 @@ open Attributes
 
 let query_command = Entry.create "vernac:query_command"
 
+let search_query = Entry.create "vernac:search_query"
+let search_queries = Entry.create "vernac:search_queries"
+
 let subprf = Entry.create "vernac:subprf"
 
 let quoted_attributes = Entry.create "vernac:quoted_attributes"
@@ -819,7 +822,7 @@ GRAMMAR EXTEND Gram
 END
 
 GRAMMAR EXTEND Gram
-  GLOBAL: command query_command class_rawexpr gallina_ext;
+  GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
 
   gallina_ext:
     [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
-- 
cgit v1.2.3