Searching for headconcl and headhyp requires manually inserting coercions to Sortclass.

[chdoc]

Description of the problem

When searching for something like the "contra" lemmas in ssr, a natural search might be headconcl:(~~ _). However, this does not return any results as ~~ _ is always boolean rather than a type, and cannot be the head of a return type. So one has to search for headconcl:(is_true (~~ _)) instead. This is a regression compared to the search function in the ssrsearch module, where the coercion to Prop/Sortclass was inserted automatically

Require Import ssr.ssrbool.
Search headconcl:(~~ _). (* nothing *)
Search headconcl:(is_true (~~ _)). (* contra lemmas *)
Search concl:(~~ _). (* a lot more results *)
Require Import ssrsearch.ssrsearch.
Search (~~ _). (* same contra lemmas as above *)

Coq Version

8.12

[herbelin]

Good remark, thanks! Don't know what would be the best. We may seize this limitation to try to type the pattern, so that coercions are inserted anywhere it is needed, and not only at the top.

[herbelin]

See #13255 for coercion support in Search. Don't hesitate if you have other suggestions.