[ssr] Searching lemmas in presence of implicit coercions

[anton-trunov]

Description of the problem

From Coq Require Import ssreflect ssrbool.

Search _ (~~ ?b -> ~~ ?c).

The search command above produces no output, but

contra  forall c b : bool, (c -> b) -> ~~ b -> ~~ c
contraNN  forall c b : bool, (c -> b) -> ~~ b -> ~~ c
contraLR  forall c b : bool, (~~ c -> ~~ b) -> b -> c
contraTT  forall c b : bool, (~~ c -> ~~ b) -> b -> c

is expected.

It looks like the search mechanism does not insert the is_true implicit coercions that are needed here to find the required lemmas. E.g.

Search _ (is_true ( ~~ ?b) -> is_true ( ~~ ?c )).

produces the desired output, but seems to be too complicated.

Coq Version

8.9.1

Thanks @llelf for bringing this to my attention.