Failing package builds with Load commands in Coq files

Expected Behavior

Coq supports the Loadcommands that reads and processes commands verbatim from some other file. For example, one might have a file moreCoefStructure.v which has a sentence:

Load mCoefStructure.

which implicitly uses another file named mCoefStructure.v. However, this latter file does not build with Coq standalone, it's solely meant to be loaded. Hence, one adds to the dune file:

(modules :standard \ mCoefStructure)

I expected dune package builds with Coq projects that use Load commands to work normally - which they do with a simple dune build.

Actual Behavior

With dune build -p <package>, the files that are only meant to be loaded are not copied into the build tree, so one gets an error message along the lines of:

(cd _build/default && coqc -R . Namespace moreCoefStructure.v)
File "./moreCoefStructure.v", line X, characters Y-Z:
Error: Can't find file hCoefStructure.v on loadpath

Reproduction

To reproduce on a real project with Dune 2.4 and Coq 8.7 or later:

git clone https://github.com/coq-community/buchberger.git
cd buchberger
git checkout v8.11.0
dune build -p coq-buchberger

Specifications

• Version of dune (output of dune --version): 2.4.0
• Version of ocaml (output of ocamlc --version): 4.09.0
• Operating system (distribution and version): Ubuntu Linux 16.04

cc: @ejgallego

Reproduce the failure in coq-community/buchberger at v8.11.0 with dune build -p coq-buchberger, then compare it with dune build. Inspect the dune file and the Load relationship between moreCoefStructure.v and mCoefStructure.v; done means package builds include load-only files in the build tree and Coq completes without a missing-file error.