I'm really lost on how to actually use multiple files in Coq. I was trying to follow these directions.
I have two files.
src/a.v
:
Definition bar: nat := 1.
src/b.v
:
Require Import a.
Definition foo := bar.
I attempt to compile as such:
coqc -R src "" src/a.v src/b.v
I get the following error:
user@machine:~/code/coq$ coqc -R src "" src/a.v src/b.v
While loading initial state:
Loading file /home/user/code/coq/src/.b.aux: aux file name mismatch
I can't find any clear information on how you actually compile with multiple files