The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> > You've already done the hard work of figuring out which type family is
> > matched with each of the different notations.
> >     
> I does not even understand what this sentence can mean.... i'm trying
> to understand
> http://www.lix.polytechnique.fr/coq/stdlib/Coq.Init.Specif.html
>   

I didn't know your context.  In reading code written by someone else, 
you might come across use of a notation where you don't know what the 
notation expands to; that would be the case where you use [Locate].  If 
you were looking at the above page in the first place, then all the 
notation definitions are right there, so there's no role for [Locate].