Search should support is:Local and blacklist local definitions by default

[andres-erbsen]

Description of the problem

Search returns internal definitions of libraries.

On top of #16915,

Require Import Znumtheory.
Search "helper".
(* Znumtheory.extgcd_rec_helper *)
Search "extgcd".
(* extgcd *)
(* Znumtheory.extgcd_rec_helper *)
(* extgcd_correct *)
(* Znumtheory.extgcd_rec *)

All fully qualified results in the above Search output are intended to be private to the implementation of the non-fully-qualified results. They should not be suggested to users looking for properties of extgcd.

Once deprecation of definitions is implemented, deprecated definitions should be excluded by default as well.

Coq Version

#16915, presumably also master and 8.16.0