The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Hi Jeremy,

You need to set up an `_CoqProject` like this:

```

-Q category Cat

category/cat.v

category/ncat.v

```

... and run `coq_makefile` to generate a Makefile. Note that if you can `make` the project, then Coq should work from Emacs just fine.

In the example I've supplied, "category" is the subdirectory you want to include, and you'd use `From Cat Require Import ...` to include a file in it.

R.

On Wed, Feb 5, 2020 at 8:09 AM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

The documentation at
https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.load
says

     This command loads the file named ident.v, searching successively
in each of the directories specified in the loadpath. (see Section
Libraries and filesystem)
but when I go to that section it doesn't tell you how to set a
"loadpath" or how to view what it is (or even what it is, so I've got to
guess it's as in other languages that I'm familiar with - and that
somehow doesn't seem to fit the case)

So how do I load a file (eg, ttt/TTT/sss.v)

Thanks

Jeremy