The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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