The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Theo,

Yes, thanks - that was exactly right.  I'd never imagined that Notation 
should be used in the context of something like Locate Library

Thanks

Jeremy

On 28/4/20 6:15 pm, Théo Zimmermann wrote:
> Hi Jeremy,
>
> The only explanation that I can see for your problem is that existsT
> is a defined as a keyword at the point where you call Locate.
>
> Example:
>
> Notation "'existsT'" := 0.
> Locate Library existsT.
>
> Otherwise, this failure doesn't make any sense since existsT is a
> valid identifier, and thus a valid global identifier (constr:global).
>
> Cheers,
> Théo
>
> Le mar. 28 avr. 2020 à 08:41, Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
>  a écrit :
> > Hi,
> >
> > Trying to use the Locate Library command I get
> >
> >   > Locate Library existsT.
> >   >                ^^^^^^^
> > Error:
> > Syntax error: [constr:global] expected after 'Library' (in [locatable]).
> >
> > I've seen this sort of gibberish before, but it's generally due to a
> > recognizable syntax error.  But here I can't seen what is wrong with the
> > way I'm using the Locate Library command, eg
> >
> > Coq < Locate Library gen.
> > gen is bound to file /home/jeremy/coq/lnt/tense-logic-in-Coq/gen.vo
> >
> > Coq < Locate Library xxx.
> > Toplevel input, characters 15-18:
> >   > Locate Library xxx.
> >   >                ^^^
> > Error: Unable to locate library xxx.
> >
> > these work as expected - what is happening here?
> >
> > Cheers,
> >
> > Jeremy