The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

it works. I had found "Locate" in the manual but it was used only with notations.

2014-10-22 15:29 GMT-03:00 Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>:

On 22/10/2014 20:29, Leonardo Rodriguez wrote:
> I have a simple question: how do you find out where a function is located,
> in which file. I know that I can do a "grep -r funcion_name *.v" in
> console, but I wonder if there is a better way (and I have several
> libraries imported that reside in others folders, then "grep" does not
> help much).

[Locate foo.] in a Coq buffer?

PMP