The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/17/2013 09:48 PM, Math Prover wrote:
> Here is my question: How does Search and SearchAbout differ in practice?
>
> The manual states:
>
> It is often difficult to remember the names of all lemmas and definitions 
> available in the current context, especially if large libraries have been 
> loaded. A convenient SearchAbout command is available to lookup all known 
> facts concerning a given predicate. For instance, if you want to know all the 
> known lemmas about the less or equal relation, just ask:
>
>
> and
>
> Another command Search displays only lemmas where the searched predicate 
> appears at the head position in the conclusion.
>    

These explanations seem to give the complete story on the difference 
between the commands.  Perhaps the issue is that you aren't familiar 
with the terminology "head position"?  The upshot in this case seems to 
be that [Search] only considers types that match your query with extra 
[forall]s added in front, whereas [SearchAbout] applies a looser rule.