fix(rocq): add error handling and hints for Rocq modules duplication

[Durbatuluk1701]

Currently, if a rocq.theory stanza and rocq.extraction stanza use the same module, we can encounter an error due to the attempted duplicate add:

$ dune build
Internal error! Please report to https://github.com/ocaml/dune/issues,
providing the file _build/trace.csexp, if possible. This includes build
commands, message logs, and file paths.
Description:
  ("Map.add_exn: key already exists",
   { key =
       { source = In_build_dir "default/theories/FactExtr.v"
       ; prefix = []
       ; name = "FactExtr"
       }
   })

This PR addresses the issue by not performing an add_exn, as well as adding hints to the raised errors to provide more helpful guidance.

Example Code

Not quite "minimal" example but hopefully good enough. Also note: this dune file will still not *fully* compile as there seems to be some issue with having a theory and extraction in the same folder?

FactProg.v:

From Stdlib Require Import Lia.

Fixpoint fact (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => n * fact n'
  end.

Fixpoint fact_tail (acc : nat) (n : nat) : nat :=
  match n with
  | 0 => acc
  | S n' => fact_tail (acc * n) n'
  end.

FactExtr.v:

Require Import FactProg.

Require Extraction.
Separate Extraction fact_tail.

dune:

(include_subdirs qualified)

(rocq.theory
 (name TestPkg)
 (package test-pkg)
 (theories Stdlib)
 (synopsis "A test package"))

(rocq.extraction
 (prelude FactExtr)
 (theories Stdlib)
 (extracted_modules FactProg Datatypes Nat))

[rlepigre-skylabs-ai]

Thanks! This looks good to me. I left a few minor comments.

[rlepigre-skylabs-ai]

Thanks for the changes, I don't have any further comments.

[Alizter]

@Durbatuluk1701 Could you add a change log entry in doc/changes?

[Alizter]

Thanks!