Allow to have a coq.extraction and coq.theory in the same directory

Desired Behavior

To the best of my knowledge, it is currently not possible to have a coq.theory and
and coq.extraction within the same directory.

The reason is the following: coq.extraction uses the flag -R . DuneExtraction even
if this flag is useless (if we had a Coq file in ., coq.extraction will not know how
to build it). But in addition it prevents the use case I propose.

If I am right, this flag can be safely removed, and if we do, my use case should work.

Example

See this test repository to have a complete example,

but in practice the dune file I am looking for to be able to write is

(coq.theory
  (modules :standard \ extract)
  (name Foo))

(coq.extraction
  (prelude extract)
  (extracted_modules extract)
  (theories Foo))

Start with the linked test repository and the example dune file to reproduce the conflict between coq.theory and coq.extraction in one directory. Inspect how the coq.extraction rule adds the -R . DuneExtraction flag, then verify whether removing it allows the example to build while preserving existing extraction behavior.