Somehow none of the Search commands seems to do anything for me. Check and About works.
I have coqtop inside an opam switch, but I know that’s not a problem because I can check my proofs normally.
I’m using VSCodium 1.65.2.
What version of Coq are you using? In older versions, there were two Search commands, and in the one provided by SSReflect, Search foo would only look for things containing foo in their conclusion, which could be confusing… See here for reference.
Otherwise, I think you would have to be a bit more specific as what you are searching if you want help… Could you design a minimal working example?
Using Coq 8.15 with, yes, ssreflect. But you say that difference is only in older versions, so 8.15 is not affected?
I’ll post an example as soon as I come across one, but it’s really simple: I select a symbol, like, say “injective_projections”, then I do the Command-Shift-P dance (VSC is not my usual editor, so I don’t remember the keys), pick Search, and … literally nothing happens. I can then open the Output tab, and it’s empty.
Also, no output from the “Prompt Search” item. I entered _assoc which is the top example in the Coq Reference manual.
Oh wait … when I enter "_assoc" (with literal quotes), Prompt Search works! So I guess the trouble must be somewhere around snarfing the selection from the editor buffer and passing it to coqtop, properly quoted.
For some symbols both Search and Prompt Search works. Example: existT. For others, Prompt Search works but Search (by selection) does not. Examples: injective_projections, proof_irrelevance.
That made me think: maybe the underscore in the symbol is the problem?