Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Search vs SearchAbout

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Search vs SearchAbout


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Search vs SearchAbout
  • Date: Sat, 18 May 2013 14:49:50 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page