coq-record-update icon indicating copy to clipboard operation
coq-record-update copied to clipboard

make COQPATH compatible

Open samuelgruetter opened this issue 4 years ago • 0 comments

(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 :wink:) 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.

samuelgruetter avatar Dec 05 '20 04:12 samuelgruetter