Currently, dune extraction is always performed. The user should be able to limit its scope with the package field (like in coq.theory)

One use-case is when the project contains several packages, some of which do not require Coq. Building non-coq packages with dune build -p pkg should be possible.