test(coq): duplicate theory prefix in COQPATH bug

This bug happens when using COQPATH so it won't affect most users. When
having two theories A.B and A.C installed, dune will erroneously fail
saying that the theory A has been defined twice.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune

@@ -0,0 +1,3 @@
+(coq.theory
+ (name A.B)
+ (package Theory1))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.8)
+(using coq 0.8)
+(package (name Theory1))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune

@@ -0,0 +1,3 @@
+(coq.theory
+ (name A.C)
+ (package Theory2))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.8)
+(using coq 0.8)
+(package (name Theory2))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t

@@ -0,0 +1,41 @@
+If we have installed theories A.B and A.C then Dune should not complain that A
+is a duplicate theory.
+
+First we install our two theories with the conflicting name prefix.
+
+  $ (cd B && dune build @install && dune install --prefix .)
+  $ (cd C && dune build @install && dune install --prefix .)
+
+We add these to COQPATH
+
+  $ export COQPATH=../B/lib/coq/user-contrib:../C/lib/coq/user-contrib:$COQPATH
+
+Now we create a theory that depends on both
+
+  $ mkdir mytheory && cd mytheory
+
+  $ cat > dune-project << EOF
+  > (lang dune 3.8)
+  > (using coq 0.8)
+  > EOF
+
+  $ cat > dune << EOF
+  > (coq.theory
+  >  (name mytheory)
+  >  (theories A.B A.C))
+  > EOF
+
+  $ cat > a.v << EOF
+  > From A.B Require a.
+  > From A.C Require a.
+  > EOF
+
+
+  $ dune build a.vo --display short
+  Error: Coq theory A is defined twice:
+  - theory A in
+    $TESTCASE_ROOT/mytheory/../B/lib/coq/user-contrib/A
+  - theory A in
+    $TESTCASE_ROOT/mytheory/../C/lib/coq/user-contrib/A
+  [1]
+