diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dir1/file3.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dir1/file3.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dune b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dune
new file mode 100644
index 00000000000..5e6e3691d54
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/dune
@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory2))
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/file2.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/coq_dir1/file2.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune
new file mode 100644
index 00000000000..8fefbfa5870
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune
@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory1))
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-project b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-project
new file mode 100644
index 00000000000..8b858cdefd7
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-workspace b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-workspace
new file mode 100644
index 00000000000..0ececa7d7ff
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.8)
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/file1.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/file1.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dir2/file6.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dir2/file6.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dune b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dune
new file mode 100644
index 00000000000..2834ddbdd3e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/dune
@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name theory4))
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/file5.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/coq_dir2/file5.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune
new file mode 100644
index 00000000000..208a2161e83
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune
@@ -0,0 +1,2 @@
+(coq.theory
+ (name theory3))
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune-project b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune-project
new file mode 100644
index 00000000000..8b858cdefd7
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/file4.v b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/project/file4.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/run.t
new file mode 100644
index 00000000000..5cf39516cc4
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/run.t
@@ -0,0 +1,120 @@
+Running "dune coq top" from different directories in a workspace. The setup is
+a workspace whose root is the root of a first project, and a second project is
+contained under directory "project".
+
+  $ unset INSIDE_DUNE
+  $ . ./util.sh
+
+Calling "dune coq top" from the workspace root.
+
+  $ coqtop_test file1.v
+  $ coqtop_test coq_dir1/file2.v
+  $ coqtop_test coq_dir1/dir1/file3.v
+  $ coqtop_test project/file4.v
+  $ coqtop_test project/coq_dir2/file5.v
+  $ coqtop_test project/coq_dir2/dir2/file6.v
+
+  $ check_build
+
+Calling "dune coq top" from the "coq_dir1" directory.
+
+  $ cd coq_dir1
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file2.v
+  $ coqtop_test dir1/file3.v
+
+  $ cd ..
+
+  $ check_build
+
+Calling "dune coq top" from the "coq_dir1/dir1" directory.
+
+  $ cd coq_dir1/dir1
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file2.v
+  $ coqtop_test ../dir1/file3.v
+  $ coqtop_test file3.v
+
+  $ cd ../..
+
+  $ check_build
+
+Calling "dune coq top" from the "project" directory.
+
+  $ cd project
+
+  $ coqtop_test ../file1.v
+  $ coqtop_test ../coq_dir1/file2.v
+  $ coqtop_test ../coq_dir1/dir1/file3.v
+  $ coqtop_test ../project/file4.v
+  $ coqtop_test ../project/coq_dir2/file5.v
+  $ coqtop_test ../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test file4.v
+  $ coqtop_test coq_dir2/file5.v
+  $ coqtop_test coq_dir2/dir2/file6.v
+
+  $ cd ..
+
+  $ check_build
+
+Calling "dune coq top" from the "project/coq_dir2" directory.
+
+  $ cd project/coq_dir2
+
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../file1.v
+  $ coqtop_test ../../coq_dir1/file2.v
+  $ coqtop_test ../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../project/file4.v
+  $ coqtop_test ../../project/coq_dir2/file5.v
+  $ coqtop_test ../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../file4.v
+  $ coqtop_test ../coq_dir2/file5.v
+  $ coqtop_test ../coq_dir2/dir2/file6.v
+  $ coqtop_test file5.v
+  $ coqtop_test dir2/file6.v
+
+  $ cd ../..
+
+  $ check_build
+
+Calling "dune coq top" from the "project/coq_dir2/dir2" directory.
+
+  $ cd project/coq_dir2/dir2
+
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../file1.v
+  $ coqtop_test ../../../coq_dir1/file2.v
+  $ coqtop_test ../../../coq_dir1/dir1/file3.v
+  $ coqtop_test ../../../project/file4.v
+  $ coqtop_test ../../../project/coq_dir2/file5.v
+  $ coqtop_test ../../../project/coq_dir2/dir2/file6.v
+
+  $ coqtop_test ../../file4.v
+  $ coqtop_test ../../coq_dir2/file5.v
+  $ coqtop_test ../../coq_dir2/dir2/file6.v
+  $ coqtop_test ../file5.v
+  $ coqtop_test ../dir2/file6.v
+  $ coqtop_test file6.v
+
+  $ cd ../../..
+
+  $ check_build
diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/util.sh b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/util.sh
new file mode 100755
index 00000000000..41f2eb85c95
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-workspace.t/util.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+export OUTPUT="$PWD/coqtop_test.tmp"
+export PWD0="$PWD"
+
+function coqtop_test() {
+  (true | (dune coq top "$1" 1>$OUTPUT 2>&1)) || cat $OUTPUT
+}
+
+function check_build() {
+  if [[ ! -d "./_build" ]]; then
+    echo "No build directory found..."
+    exit 1
+  fi
+
+  if [[ $(find . -name _build -type d | wc -l) > 1 ]]; then
+    echo "More than one _build directory..."
+    exit 1
+  fi
+}