Desired Behavior

Using dune coq top and dune build on the same source file should use different flags:
dune coq top should let coqtop load ~/.coqrc — to this end, it should not pass the -q flag.

Contrast with dune build, which correctly includes -q in Coq's :standard flag to skip loading .coqrc.

This follows existing practice with coq_makefile and editors and the documented purpose of coqrc: provide custom settings for interactive exploration, while keeping building .vo files reproducible.

I suggested this on Zulip and @Alizter asked for a ticket, so here it is.