You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(Note: so far I've only used coq-record-update in one example file in riscv-coq which has become obsolete in the meantime, so the issue I'm raising here is not blocking me in any way, I'm just opening it because maybe other projects (including one of mine, who knows 😉) might run into this issue at some point in the future).
Some projects (eg fiat-crypto) obtain their dependencies by adding directories to the COQPATH variable (rather than using -Q or -R arguments to coqc). However, this only works if each project is in a directory named the same as the logical name used to import from it, i.e. to enable such projects to depend on coq-record-update, the .v files in coq-record-update/src/ should be moved to coq-record-update/src/RecordUpdate.
The text was updated successfully, but these errors were encountered:
(Note: so far I've only used coq-record-update in one example file in riscv-coq which has become obsolete in the meantime, so the issue I'm raising here is not blocking me in any way, I'm just opening it because maybe other projects (including one of mine, who knows 😉) might run into this issue at some point in the future).
Some projects (eg fiat-crypto) obtain their dependencies by adding directories to the
COQPATH
variable (rather than using-Q
or-R
arguments tocoqc
). However, this only works if each project is in a directory named the same as the logical name used to import from it, i.e. to enable such projects to depend on coq-record-update, the.v
files incoq-record-update/src/
should be moved tocoq-record-update/src/RecordUpdate
.The text was updated successfully, but these errors were encountered: