3 files changed, 1 insertions, 19 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 35fecfb0a5..ccdf5fa68e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -350,7 +350,7 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc (None, []) with
-          | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n ->
+          | Constrexpr.Number n, _ when NumTok.Signed.is_int n ->
             int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index a49a5e8b28..99cf197b78 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -304,21 +304,6 @@ END
 
 {
 
-  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
-            "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
 }
 
@@ -328,7 +313,6 @@ GRAMMAR EXTEND Gram
   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) }
       ] ]
diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli
index 93339313f0..327a2d4660 100644
--- a/plugins/ssr/ssrvernac.mli
+++ b/plugins/ssr/ssrvernac.mli
@@ -9,5 +9,3 @@
 (************************************************************************)
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-
-val warn_search_moved_enabled : bool ref