Merge PR #12341: [search] [ssr] Emit deprecated message when calling search from ssreflect

Reviewed-by: Zimmi48
Ack-by: gares

1 files changed, 4 insertions, 1 deletions

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 ->