From 2a803690d76724fd7c97288f208f3a1faf98eca1 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 27 Mar 2020 21:55:37 -0700
Subject: Remove SearchAbout command, deprecated in 8.5

---
 plugins/ssr/ssrvernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index df6189f212..4b78e64d98 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with
 | [] -> accu
 | (flag, arg) :: rem ->
   fun gr env typ ->
-    let ans = Search.search_about_filter arg gr env typ in
+    let ans = Search.search_filter arg gr env typ in
     (if flag then ans else not ans) && interp_search_about rem accu gr env typ
 
 let interp_search_arg arg =
-- 
cgit v1.2.3