The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 18/05/2013 17:11, Jason Gross wrote:
> Adam, your explanation works for trunk, where [Search] gives me
> things of type [Z -> Z -> bool], and [SearchAbout] gives me things of
> type, e.g., [Morphisms.Proper (Morphisms.respectful eq Z.eqf)
> Z.testbit].

For your information, Search and SearchAbout have been merged in trunk, 
as CHANGES states:

> Command "Search" has been renamed into "SearchHead". The command name
> "Search" now behaves like former "SearchAbout". The latter name is
> deprecated.

Therefore, trying to understand the difference between both using trunk 
won't be fruitful...

PMP