aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/search.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/search.ml b/parsing/search.ml
index e225d59a48..b9982ad3d2 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -214,7 +214,8 @@ let search_about_item (itemref,typ) = function
let raw_search_about filter_modules display_function l =
let filter ref' env typ =
filter_modules ref' env typ &&
- List.for_all (search_about_item (ref',typ)) l
+ List.for_all (search_about_item (ref',typ)) l &&
+ not (string_string_contains (name_of_reference ref') "_subproof")
in
gen_filtered_search filter display_function