The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I was actually using the trunk of https://github.com/HoTT/coq; sorry for the confusion.  It looks like this corresponds roughly to f5ab2e37b0609d8edb8d65dfae49741442a90657, which is before the [SearchHead] command was added.

-Jason

On Sat, May 18, 2013 at 12:15 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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