The Coq mailing list

[Dan Frumin <dfrumin AT cs.ru.nl>]

Hi Jeremy,

I don't know why -I doesn't work, but I think using -Q does the trick (at 
least with my version of Coq): I replaced

    -I ../lnt/tense-logic-in-Coq/

with
    -Q ../lnt/tense-logic-in-Coq/ TL

and then in dd_fc.v used `Require Import TL.genT`



Best,
Dan


On 26-04-2020 16:09, Jeremy Dawson wrote:
> Hi,
>
> I've constructed a _CoqProject file as follows
>
> -I ../lnt/tense-logic-in-Coq/
> -I ../gen/
> ../lnt/tense-logic-in-Coq/gen.v
> ../lnt/tense-logic-in-Coq/genT.v
> ../lnt/tense-logic-in-Coq/List_lemmasT.v
> ../lnt/tense-logic-in-Coq/lntT.v
> ../lnt/tense-logic-in-Coq/swappedT.v
> ../lnt/tense-logic-in-Coq/ddT.v
> ../lnt/tense-logic-in-Coq/dd_fc.v
> ../lnt/tense-logic-in-Coq/lntacsT.v
> ../gen/rtcT.v
> ../gen/gstep.v
> ../gen/gentree.v
> gen_ext.v
> k4.v
> k4_exch.v
> k4_inv.v
> k4_ctr.v
> k4_ca.v
>
> I then run
>   make -f Makefile
> and get the following messages
> COQC ../lnt/tense-logic-in-Coq/dd_fc.v
> File "../lnt/tense-logic-in-Coq/dd_fc.v", line 12, characters 15-19:
> Error: Unable to locate library genT.
>
> (in fact the file
> ../lnt/tense-logic-in-Coq/genT.v
> exists)
>
> What do I need to put in the _CoqProject file to make this work?
>
> Thanks
>
> Jeremy