The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Indeed -I is for ocaml files (for plugins)

Gaëtan Gilbert

On 26/04/2020 16:23, Dan Frumin wrote:
> 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