aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrvernac.mlg2
1 files changed, 1 insertions, 1 deletions
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 =