Extraction directory and Coq files in theories
The current project doesn't have the Coq files living in theories
because if we put them there the following happens:
-
Extraction "ml/extracted" f.
works withmake
but not Proof General -
Extraction "../ml/extracted" f.
works with Proof General but notmake
I complained about this in Zulip and the conclusion was that a Extraction Directory
command would solve this and was on the way. This command is now available in Coq 8.19, so it could be used to reorganize our Coq files into theories
.