diff --git a/bin/coqtop.ml b/bin/coqtop.ml
index b836bfe2c0c7..76219bc1c707 100644
--- a/bin/coqtop.ml
+++ b/bin/coqtop.ml
@@ -96,6 +96,7 @@ let term =
               in
               let* (_ : unit * Dep.Fact.t Dep.Map.t) =
                 let deps =
+                  let boot_type = Resolve.Memo.return boot_type in
                   Dune_rules.Coq_rules.deps_of ~dir ~boot_type coq_module
                 in
                 Action_builder.run deps Eager
diff --git a/bin/import.ml b/bin/import.ml
index 2bbf30502f29..238bedd51f4f 100644
--- a/bin/import.ml
+++ b/bin/import.ml
@@ -28,6 +28,7 @@ module Workspace = Dune_rules.Workspace
 module Cached_digest = Dune_engine.Cached_digest
 module Targets = Dune_engine.Targets
 module Profile = Dune_rules.Profile
+module Resolve = Dune_rules.Resolve
 module Log = Dune_util.Log
 module Dune_rpc = Dune_rpc_private
 module Graph = Dune_graph.Graph
diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
index 5a7155ecae6c..6a3ad4224037 100644
--- a/src/dune_rules/coq_lib.ml
+++ b/src/dune_rules/coq_lib.ml
@@ -5,19 +5,51 @@ open Import
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
-(* At some point we may want to reify this into resolved status, for example:
+module Id = struct
+  module T = struct
+    type t =
+      { path : Path.Build.t
+      ; name : Coq_lib_name.t
+      }
 
-   ; libraries : Lib.t list Or_exn.t
+    let compare t { path; name } =
+      let open Ordering.O in
+      let= () = Path.Build.compare t.path path in
+      Coq_lib_name.compare t.name name
+
+    let to_dyn { path; name } =
+      Dyn.(
+        record
+          [ ("path", Path.Build.to_dyn path)
+          ; ("name", Coq_lib_name.to_dyn name)
+          ])
+  end
+
+  include T
+
+  let pp { path; name } =
+    Pp.concat ~sep:Pp.space
+      [ Pp.textf "theory %s in" (Coq_lib_name.to_string name)
+      ; Path.pp (Path.build path)
+      ]
+
+  let create ~path ~name = { path; name }
+
+  module C = Comparable.Make (T)
+  module Top_closure = Top_closure.Make (C.Set) (Resolve)
+
+  let top_closure ~key ~deps xs = Top_closure.top_closure ~key ~deps xs
+end
 
-   etc.. *)
 type t =
   { name : Loc.t * Coq_lib_name.t
-  ; wrapper : string
+  ; boot : t option Resolve.t
+  ; id : Id.t
   ; implicit : bool (* Only useful for the stdlib *)
   ; src_root : Path.Build.t
   ; obj_root : Path.Build.t
-  ; theories : (Loc.t * Coq_lib_name.t) list
-  ; libraries : (Loc.t * Lib_name.t) list
+  ; theories : (Loc.t * t) list Resolve.t
+  ; libraries : (Loc.t * Lib.t) list Resolve.t
   ; package : Package.t option
   }
 
@@ -25,10 +57,6 @@ let name l = snd l.name
 
 let implicit l = l.implicit
 
-let location l = fst l.name
-
-let wrapper l = l.wrapper
-
 let src_root l = l.src_root
 
 let obj_root l = l.obj_root
@@ -38,128 +66,276 @@ let libraries l = l.libraries
 let package l = l.package
 
 module Error = struct
-  let make ?loc ?hints paragraphs =
-    Error (User_error.E (User_error.make ?loc ?hints paragraphs))
+  let annots =
+    User_message.Annots.singleton User_message.Annots.needs_stack_trace ()
 
-  let duplicate_theory_name theory =
-    let loc, name = theory.Coq_stanza.Theory.name in
+  let duplicate_theory_name (loc, name) =
     let name = Coq_lib_name.to_string name in
-    make ~loc [ Pp.textf "Duplicate theory name: %s" name ]
+    User_error.raise ~loc [ Pp.textf "Duplicate theory name: %s" name ]
+
+  let incompatible_boot id id' =
+    let pp_lib (id : Id.t) = Pp.seq (Pp.text "- ") (Id.pp id) in
+    User_message.make ~annots
+      [ Pp.textf "The following theories use incompatible boot libraries"
+      ; pp_lib id'
+      ; pp_lib id
+      ]
+    |> Resolve.fail
 
   let theory_not_found ~loc name =
     let name = Coq_lib_name.to_string name in
-    make ~loc [ Pp.textf "Theory %s not found" name ]
-
-  let private_deps_not_allowed ~loc private_dep =
-    let name = Coq_lib_name.to_string (name private_dep) in
-    make ~loc
-      [ Pp.textf
-          "Theory %S is private, it cannot be a dependency of a public theory. \
-           You need to associate %S to a package."
-          name name
-      ]
+    Resolve.Memo.fail
+    @@ User_message.make ~annots ~loc [ Pp.textf "Theory %s not found" name ]
 
-  let duplicate_boot_lib ~loc boot_theory =
-    let name =
-      Coq_lib_name.to_string (snd boot_theory.Coq_stanza.Theory.name)
-    in
-    make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ]
+  let private_deps_not_allowed ~loc name =
+    let name = Coq_lib_name.to_string name in
+    Resolve.Memo.fail
+    @@ User_message.make ~loc
+         [ Pp.textf
+             "Theory %S is private, it cannot be a dependency of a public \
+              theory. You need to associate %S to a package."
+             name name
+         ]
 
-  let cycle_found ~loc cycle =
-    make ~loc
-      [ Pp.textf "Cycle found"
-      ; Pp.enumerate cycle ~f:(fun t ->
-            Pp.text (Coq_lib_name.to_string (snd t.name)))
+  let duplicate_boot_lib theories =
+    let open Coq_stanza.Theory in
+    let name (_dir, t) =
+      let name = Coq_lib_name.to_string (snd t.name) in
+      Pp.textf "%s at %s" name (Loc.to_file_colon_line t.buildable.loc)
+    in
+    User_error.raise
+      [ Pp.textf "Cannot have more than one boot theory in scope:"
+      ; Pp.enumerate theories ~f:name
       ]
 end
 
 module DB = struct
   type lib = t
 
-  type nonrec t =
-    { boot : (Loc.t * t) option
-    ; libs : t Coq_lib_name.Map.t
+  type t =
+    { parent : t option
+    ; resolve :
+        Coq_lib_name.t -> (Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t) option
+    ; boot : (Loc.t * lib Resolve.t Memo.Lazy.t) option
     }
 
-  let boot_library { boot; _ } = boot
-
-  let create_from_stanza ((dir, s) : Path.Build.t * Coq_stanza.Theory.t) =
-    let name = snd s.name in
-    ( name
-    , { name = s.name
-      ; wrapper = Coq_lib_name.wrapper name
-      ; implicit = s.boot
-      ; obj_root = dir
-      ; src_root = dir
-      ; theories = s.buildable.theories
-      ; libraries = s.buildable.libraries
-      ; package = s.package
-      } )
+  module rec R : sig
+    val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t
+  end = struct
+    open R
+
+    let rec boot coq_db =
+      match coq_db.boot with
+      | Some (_, boot) ->
+        Memo.Lazy.force boot |> Resolve.Memo.map ~f:Option.some
+      | None -> (
+        match coq_db.parent with
+        | None -> Resolve.Memo.return None
+        | Some parent -> boot parent)
+
+    let create_from_stanza =
+      let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) =
+        let id = Id.create ~path:dir ~name:(snd s.name) in
+        let open Memo.O in
+        let* boot = if s.boot then Resolve.Memo.return None else boot coq_db in
+        let allow_private_deps = Option.is_none s.package in
+        let+ libraries =
+          Resolve.Memo.List.map s.buildable.libraries ~f:(fun (loc, lib) ->
+              let open Resolve.Memo.O in
+              let* lib = Lib.DB.resolve db (loc, lib) in
+              let+ () =
+                Resolve.Memo.lift
+                @@
+                if allow_private_deps then Resolve.return ()
+                else
+                  match
+                    let info = Lib.info lib in
+                    let status = Lib_info.status info in
+                    Lib_info.Status.is_private status
+                  with
+                  | false -> Resolve.return ()
+                  | true ->
+                    Resolve.fail
+                    @@ User_message.make ~loc
+                         [ Pp.textf
+                             "private theory %s may not depend on a public \
+                              library"
+                             (Coq_lib_name.to_string (snd s.name))
+                         ]
+              in
+              (loc, lib))
+        and+ theories =
+          let check_boot (lib : lib) =
+            let open Resolve.O in
+            let* boot = boot in
+            match boot with
+            | None -> Resolve.return ()
+            | Some boot -> (
+              let* boot' = lib.boot in
+              match boot' with
+              | None -> Resolve.return ()
+              | Some boot' -> (
+                match Id.compare boot.id boot'.id with
+                | Eq -> Resolve.return ()
+                | _ -> Error.incompatible_boot lib.id id))
+          in
+          Resolve.Memo.List.map s.buildable.theories ~f:(fun (loc, theory) ->
+              let open Resolve.Memo.O in
+              let* theory = resolve coq_db (loc, theory) in
+              let* () = Resolve.Memo.lift @@ check_boot theory in
+              let+ () =
+                if allow_private_deps then Resolve.Memo.return ()
+                else
+                  match theory.package with
+                  | Some _ -> Resolve.Memo.return ()
+                  | None ->
+                    Error.private_deps_not_allowed ~loc (snd theory.name)
+              in
+              (loc, theory))
+        in
+        let theories =
+          let open Resolve.O in
+          let* boot = boot in
+          match boot with
+          | None -> theories
+          | Some boot ->
+            let+ theories = theories in
+            (* TODO: if lib is boot, don't add boot dep *)
+            (* maybe use the loc for boot? *)
+            (Loc.none, boot) :: theories
+        in
+        let map_error x =
+          let human_readable_description () = Id.pp id in
+          Resolve.push_stack_frame ~human_readable_description x
+        in
+        let theories = map_error theories in
+        let libraries = map_error libraries in
+        { name = s.name
+        ; boot
+        ; id
+        ; implicit = s.boot
+        ; obj_root = dir
+        ; src_root = dir
+        ; theories
+        ; libraries
+        ; package = s.package
+        }
+      in
+      let module Input = struct
+        type nonrec t = t * Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t
+
+        let equal (coq_db, ml_db, path, stanza) (coq_db', ml_db', path', stanza')
+            =
+          coq_db == coq_db' && ml_db == ml_db'
+          && Path.Build.equal path path'
+          && stanza == stanza'
+
+        let hash = Poly.hash
+
+        let to_dyn = Dyn.opaque
+      end in
+      let memo =
+        Memo.create "create-from-stanza"
+          ~human_readable_description:(fun (_, _, path, theory) ->
+            Id.pp (Id.create ~path ~name:(snd theory.name)))
+          ~input:(module Input)
+          create_from_stanza_impl
+      in
+      fun coq_db db dir stanza -> Memo.exec memo (coq_db, db, dir, stanza)
+
+    let rec find coq_db (loc, name) =
+      match coq_db.resolve name with
+      | Some s -> Some s
+      | None -> (
+        match coq_db.parent with
+        | None -> None
+        | Some parent -> find parent (loc, name))
+
+    let resolve coq_db (loc, name) =
+      match find coq_db (loc, name) with
+      | None -> Error.theory_not_found ~loc name
+      | Some (db, dir, stanza) ->
+        let open Memo.O in
+        let+ theory = create_from_stanza coq_db db dir stanza in
+        let open Resolve.O in
+        let* (_ : (Loc.t * Lib.t) list) = theory.libraries in
+        let+ (_ : (Loc.t * lib) list) = theory.theories in
+        theory
+  end
+
+  open R
+
+  let boot_library t =
+    match t.boot with
+    | None -> Resolve.Memo.return None
+    | Some (loc, lib) ->
+      let open Memo.O in
+      let+ lib = Memo.Lazy.force lib in
+      Resolve.map lib ~f:(fun lib -> Some (loc, lib))
 
   (* Should we register errors and printers, or raise is OK? *)
-  let create_from_coqlib_stanzas sl =
-    let libs =
-      match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with
-      | Ok m -> m
-      | Error (_name, _w1, (_, w2)) ->
-        Result.ok_exn (Error.duplicate_theory_name w2)
-    in
+  let create_from_coqlib_stanzas ~(parent : t option) ~find_db sl =
+    let t = Fdecl.create Dyn.opaque in
     let boot =
-      match List.find_all ~f:(fun (_, s) -> s.Coq_stanza.Theory.boot) sl with
-      | [] -> None
-      | [ l ] -> Some ((snd l).buildable.loc, snd (create_from_stanza l))
-      | _ :: (_, s2) :: _ ->
-        Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2)
+      let boot =
+        match List.find_all ~f:(fun (_, s) -> s.Coq_stanza.Theory.boot) sl with
+        | [] -> None
+        | [ (_, stanza) ] -> Some stanza.name
+        | ts -> Error.duplicate_boot_lib ts
+      in
+      match boot with
+      | None -> None
+      | Some (loc, name) ->
+        let lib =
+          Memo.lazy_ (fun () ->
+              let t = Fdecl.get t in
+              resolve t (loc, name))
+        in
+        Some (loc, lib)
     in
-    { boot; libs }
-
-  let resolve ?(allow_private_deps = true) db (loc, name) =
-    match Coq_lib_name.Map.find db.libs name with
-    | Some s ->
-      if (not allow_private_deps) && Option.is_none s.package then
-        Error.private_deps_not_allowed ~loc s
-      else Ok s
-    | None -> Error.theory_not_found ~loc name
-
-  let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name))
-
-  module Coq_lib_closure = Top_closure.Make (String.Set) (Or_exn)
-
-  let add_boot db theories =
-    match db.boot with
-    | None -> theories
-    (* XXX: Note that this means that we will prefix Coq with -Q, not sure we
-       want to do that (yet), but seems like good practice. *)
-    | Some (loc, stdlib) -> (loc, snd stdlib.name) :: theories
-
-  let top_closure db theories ~allow_private_deps ~loc =
-    let open Result.O in
-    let* theories =
-      add_boot db theories
-      |> Result.List.map ~f:(resolve ~allow_private_deps db)
+    let resolve =
+      let map =
+        match
+          Coq_lib_name.Map.of_list_map sl ~f:(fun (dir, theory) ->
+              (snd theory.name, (dir, theory)))
+        with
+        | Ok m -> m
+        | Error (_name, _w1, (_, w2)) -> Error.duplicate_theory_name w2.name
+      in
+      fun name ->
+        match Coq_lib_name.Map.find map name with
+        | None -> None
+        | Some (dir, theory) -> Some (find_db dir, dir, theory)
     in
-    let key (t : lib) = Coq_lib_name.to_string (snd t.name) in
-    let deps (t : lib) =
-      Result.List.map ~f:(resolve ~allow_private_deps db) t.theories
+    Fdecl.set t { boot; resolve; parent };
+    Fdecl.get t
+
+  let find_many t ~loc =
+    Resolve.Memo.List.map ~f:(fun name -> resolve t (loc, name))
+
+  let top_closure theories =
+    let key (t : lib) = t.id in
+    let deps (t : lib) = t.theories |> Resolve.map ~f:(List.map ~f:snd) in
+    let open Resolve.O in
+    Id.top_closure theories ~key ~deps >>= function
+    | Ok s -> Resolve.return s
+    | Error _ -> assert false
+
+  let requires_for_user_written db theories =
+    let open Memo.O in
+    let+ theories =
+      Resolve.Memo.List.map theories ~f:(fun name -> resolve db name)
     in
-    match Coq_lib_closure.top_closure theories ~key ~deps with
-    | Ok (Ok s) -> Ok s
-    | Ok (Error cycle) -> Error.cycle_found ~loc cycle
-    | Error exn -> Error exn
-
-  let requires db (t : lib) : lib list Or_exn.t =
-    let allow_private_deps = Option.is_none t.package in
-    let loc = location t in
-    top_closure db t.theories ~loc ~allow_private_deps
-
-  let requires_for_user_written db = function
-    | [] -> Ok []
-    | start :: xs as theories ->
-      let loc =
-        let stop = Option.value (List.last xs) ~default:start in
-        Loc.span (fst start) (fst stop)
-      in
-      top_closure db theories ~loc ~allow_private_deps:true
+    Resolve.O.(theories >>= top_closure)
 
   let resolve db l = resolve db l
 end
+
+let top_closure_of_theory t =
+  let open Resolve.O in
+  let* theories = t.theories in
+  let theories = List.map theories ~f:snd in
+  DB.top_closure theories
+
+(* XXX confusing name. it refers to the closure *)
+let requires (t : t) = top_closure_of_theory t
diff --git a/src/dune_rules/coq_lib.mli b/src/dune_rules/coq_lib.mli
index 5ac26f80baf8..af1c1f9f8b53 100644
--- a/src/dune_rules/coq_lib.mli
+++ b/src/dune_rules/coq_lib.mli
@@ -10,11 +10,8 @@ val name : t -> Coq_lib_name.t
 
 val implicit : t -> bool
 
-(* this is not really a wrapper for the prefix path *)
-val wrapper : t -> string
-
 (** ml libraries *)
-val libraries : t -> (Loc.t * Lib_name.t) list
+val libraries : t -> (Loc.t * Lib.t) list Resolve.t
 
 val src_root : t -> Path.Build.t
 
@@ -22,24 +19,27 @@ val obj_root : t -> Path.Build.t
 
 val package : t -> Package.t option
 
+(** Return the list of dependencies needed for compiling this library *)
+val requires : t -> t list Resolve.t
+
 module DB : sig
-  type lib
+  type lib := t
 
   type t
 
   val create_from_coqlib_stanzas :
-    (Path.Build.t * Coq_stanza.Theory.t) list -> t
-
-  val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t
+       parent:t option
+    -> find_db:(Path.Build.t -> Lib.DB.t)
+    -> (Path.Build.t * Coq_stanza.Theory.t) list
+    -> t
 
-  val boot_library : t -> (Loc.t * lib) option
+  val find_many :
+    t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Resolve.Memo.t
 
-  val resolve : t -> Loc.t * Coq_lib_name.t -> lib Or_exn.t
+  val boot_library : t -> (Loc.t * lib) option Resolve.Memo.t
 
-  (** Return the list of dependencies needed for compiling this library *)
-  val requires : t -> lib -> lib list Or_exn.t
+  val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t
 
   val requires_for_user_written :
-    t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t
+    t -> (Loc.t * Coq_lib_name.t) list -> lib list Resolve.Memo.t
 end
-with type lib := t
diff --git a/src/dune_rules/coq_lib_name.ml b/src/dune_rules/coq_lib_name.ml
index c0342ccc1eb3..abbbc6ccab0e 100644
--- a/src/dune_rules/coq_lib_name.ml
+++ b/src/dune_rules/coq_lib_name.ml
@@ -8,6 +8,8 @@ open! Import
 (* Coq Directory Path *)
 type t = string list
 
+let compare = List.compare ~compare:String.compare
+
 let to_string x = String.concat ~sep:"." x
 
 let to_dir x = String.concat ~sep:"/" x
diff --git a/src/dune_rules/coq_lib_name.mli b/src/dune_rules/coq_lib_name.mli
index 235dc7b48210..7f0df9dae970 100644
--- a/src/dune_rules/coq_lib_name.mli
+++ b/src/dune_rules/coq_lib_name.mli
@@ -10,6 +10,8 @@ open Import
 (** A Coq library name is a dot-separated list of Coq module identifiers. *)
 type t
 
+val compare : t -> t -> Ordering.t
+
 (** Returns the wrapper name, a dot-separated list of Coq module identifies *)
 val wrapper : t -> string
 
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 1569c190121b..fd0d0284b1ba 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -68,7 +68,7 @@ module Bootstrap = struct
     | Some (_loc, lib) -> (
       (* This is here as an optimization, TODO; replace with per_file flags *)
       let init =
-        String.equal (Coq_lib.wrapper lib) wrapper_name
+        String.equal (Coq_lib_name.wrapper (Coq_lib.name lib)) wrapper_name
         && Option.equal String.equal
              (List.hd_opt (Coq_module.prefix coq_module))
              (Some "Init")
@@ -111,11 +111,11 @@ module Context = struct
     ; dir : Path.Build.t
     ; expander : Expander.t
     ; buildable : Buildable.t
-    ; theories_deps : Coq_lib.t list Resolve.t
+    ; theories_deps : Coq_lib.t list Resolve.Memo.t
     ; mlpack_rule : unit Action_builder.t
-    ; ml_flags : 'a Command.Args.t
+    ; ml_flags : 'a Command.Args.t Resolve.Memo.t
     ; scope : Scope.t
-    ; boot_type : Bootstrap.t
+    ; boot_type : Bootstrap.t Resolve.Memo.t
     ; build_dir : Path.Build.t
     ; profile_flags : string list Action_builder.t
     ; mode : Coq_mode.t
@@ -133,27 +133,35 @@ module Context = struct
 
   let theories_flags =
     let setup_theory_flag lib =
-      let wrapper = Coq_lib.wrapper lib in
       let dir = Coq_lib.src_root lib in
       let binding_flag = if Coq_lib.implicit lib then "-R" else "-Q" in
-      [ Command.Args.A binding_flag; Path (Path.build dir); A wrapper ]
+      [ Command.Args.A binding_flag
+      ; Path (Path.build dir)
+      ; A (Coq_lib.name lib |> Coq_lib_name.wrapper)
+      ]
     in
     fun t ->
-      Resolve.args
-        (let open Resolve.O in
+      Resolve.Memo.args
+        (let open Resolve.Memo.O in
         let+ libs = t.theories_deps in
         Command.Args.S (List.concat_map libs ~f:setup_theory_flag))
 
   let coqc_file_flags cctx =
     let file_flags =
-      [ cctx.ml_flags
+      [ Command.Args.Dyn (Resolve.Memo.read cctx.ml_flags)
       ; theories_flags cctx
       ; Command.Args.A "-R"
       ; Path (Path.build cctx.dir)
       ; A cctx.wrapper_name
       ]
     in
-    [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ]
+    [ Command.Args.Dyn
+        (Resolve.Memo.map
+           ~f:(fun b -> Command.Args.S (Bootstrap.flags b))
+           cctx.boot_type
+        |> Resolve.Memo.read)
+    ; S file_flags
+    ]
 
   let coqc_native_flags cctx : _ Command.Args.t =
     match cctx.mode with
@@ -199,17 +207,26 @@ module Context = struct
       ; A cctx.wrapper_name
       ]
     in
-    [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ]
+    [ Command.Args.Dyn
+        (Resolve.Memo.map
+           ~f:(fun b -> Command.Args.S (Bootstrap.flags b))
+           cctx.boot_type
+        |> Resolve.Memo.read)
+    ; S file_flags
+    ]
 
   (* compute include flags and mlpack rules *)
-  let setup_ml_deps ~lib_db libs theories =
+  let setup_ml_deps libs theories =
     (* Pair of include flags and paths to mlpack *)
     let libs =
       let open Resolve.Memo.O in
-      let* theories = Resolve.Memo.lift theories in
-      let libs = libs @ List.concat_map ~f:Coq_lib.libraries theories in
-      let* libs = libs_of_coq_deps ~lib_db libs in
-      Lib.closure ~linking:false libs
+      let* theories = theories in
+      let* theories =
+        Resolve.Memo.lift
+        @@ Resolve.List.concat_map ~f:Coq_lib.libraries theories
+      in
+      let libs = libs @ theories in
+      Lib.closure ~linking:false (List.map ~f:snd libs)
     in
     ( Resolve.Memo.args (Resolve.Memo.map libs ~f:Util.include_flags)
     , let open Action_builder.O in
@@ -225,12 +242,10 @@ module Context = struct
     let+ coq_sources = Dir_contents.coq dir_contents in
     Coq_sources.directories coq_sources ~name
 
-  let setup_native_theory_includes ~sctx ~mode
-      ~(theories_deps : Coq_lib.t list Resolve.t) ~theory_dirs =
+  let setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs =
     match mode with
     | Coq_mode.Native ->
-      Resolve.Memo.bind (Resolve.Memo.lift theories_deps)
-        ~f:(fun theories_deps ->
+      Resolve.Memo.bind theories_deps ~f:(fun theories_deps ->
           let+ l =
             Memo.parallel_map theories_deps ~f:(fun lib ->
                 let+ theory_dirs = directories_of_lib ~sctx lib in
@@ -249,7 +264,22 @@ module Context = struct
     let lib_db = Scope.libs scope in
     (* ML-level flags for depending libraries *)
     let ml_flags, mlpack_rule =
-      setup_ml_deps ~lib_db buildable.libraries theories_deps
+      let res =
+        let open Resolve.Memo.O in
+        let+ libs =
+          Resolve.Memo.List.map buildable.libraries ~f:(fun (loc, name) ->
+              let+ lib = Lib.DB.resolve lib_db (loc, name) in
+              (loc, lib))
+        in
+        setup_ml_deps libs theories_deps
+      in
+      let ml_flags = Resolve.Memo.map res ~f:fst in
+      let mlpack_rule =
+        let open Action_builder.O in
+        let* _, mlpack_rule = Resolve.Memo.read res in
+        mlpack_rule
+      in
+      (ml_flags, mlpack_rule)
     in
     let mode = select_native_mode ~sctx ~buildable in
     let* native_includes =
@@ -274,7 +304,7 @@ module Context = struct
     ; mlpack_rule
     ; ml_flags
     ; scope
-    ; boot_type = Bootstrap.No_boot
+    ; boot_type = Resolve.Memo.return Bootstrap.No_boot
     ; build_dir = (Super_context.context sctx).build_dir
     ; profile_flags
     ; mode
@@ -283,8 +313,9 @@ module Context = struct
     }
 
   let for_module t coq_module =
-    let boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in
     let boot_type =
+      let open Resolve.Memo.O in
+      let+ boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in
       Bootstrap.get ~boot_lib ~wrapper_name:t.wrapper_name coq_module
     in
     { t with boot_type }
@@ -341,9 +372,11 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module
 let deps_of ~dir ~boot_type coq_module =
   let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
   Action_builder.dyn_paths_unit
-    (Action_builder.map
-       (Action_builder.lines_of (Path.build stdout_to))
-       ~f:(parse_coqdep ~dir ~boot_type ~coq_module))
+    (let open Action_builder.O in
+    let* boot_type = Resolve.Memo.read boot_type in
+    Action_builder.map
+      (Action_builder.lines_of (Path.build stdout_to))
+      ~f:(parse_coqdep ~dir ~boot_type ~coq_module))
 
 let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
   (* coqdep needs the full source + plugin's mlpack to be present :( *)
@@ -422,7 +455,7 @@ let coqdoc_rule (cctx : _ Context.t) ~sctx ~name:(_, name) ~file_flags ~mode
   let file_flags =
     let globs =
       let open Action_builder.O in
-      let* theories_deps = Resolve.read theories_deps in
+      let* theories_deps = Resolve.Memo.read theories_deps in
       Action_builder.of_memo
       @@
       let open Memo.O in
@@ -493,7 +526,7 @@ let source_rule ~sctx theories =
      tree to produce correct dependencies, including those of dependencies *)
   Action_builder.dyn_paths_unit
     (let open Action_builder.O in
-    let* theories = Resolve.read theories in
+    let* theories = Resolve.Memo.read theories in
     let+ l =
       Action_builder.List.map theories ~f:(coq_modules_of_theory ~sctx)
     in
@@ -503,12 +536,13 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
   let coq_lib_db = Scope.coq_libs scope in
-  let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in
+  let theory = Coq_lib.DB.resolve coq_lib_db s.name in
   let* coq_dir_contents = Dir_contents.coq dir_contents in
   let* cctx =
-    let wrapper_name = Coq_lib.wrapper theory in
+    let wrapper_name = Coq_lib_name.wrapper name in
     let theories_deps =
-      Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result
+      Resolve.Memo.bind theory ~f:(fun theory ->
+          Resolve.Memo.lift @@ Coq_lib.requires theory)
     in
     let theory_dirs =
       Coq_sources.directories coq_dir_contents ~name |> Path.Build.Set.of_list
@@ -521,7 +555,8 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   let coq_modules = Coq_sources.library coq_dir_contents ~name in
   let source_rule =
     let theories =
-      let open Resolve.O in
+      let open Resolve.Memo.O in
+      let* theory = theory in
       let+ theories = cctx.theories_deps in
       theory :: theories
     in
@@ -554,12 +589,13 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
   let coq_lib_db = Scope.coq_libs scope in
-  let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in
+  let theory = Coq_lib.DB.resolve coq_lib_db s.name in
   let* coq_dir_contents = Dir_contents.coq dir_contents in
-  let+ cctx =
-    let wrapper_name = Coq_lib.wrapper theory in
+  let* cctx =
+    let wrapper_name = Coq_lib_name.wrapper name in
     let theories_deps =
-      Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result
+      Resolve.Memo.bind theory ~f:(fun theory ->
+          Resolve.Memo.lift @@ Coq_lib.requires theory)
     in
     let theory_dirs = Coq_sources.directories coq_dir_contents ~name in
     let theory_dirs = Path.Build.Set.of_list theory_dirs in
@@ -568,7 +604,8 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
       s.buildable
   in
   let cctx = Context.for_module cctx coq_module in
-  (Context.coqc_file_flags cctx, cctx.boot_type)
+  let+ boot_type = Resolve.Memo.read_memo cctx.boot_type in
+  (Context.coqc_file_flags cctx, boot_type)
 
 (******************************************************************************)
 (* Install rules *)
@@ -599,6 +636,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) =
                Path.Local.(to_string (relative dst_dir plugin_file_basename))
              in
              let entry = Install.Entry.make Section.Lib_root ~dst plugin_file in
+             (* TODO this [loc] should come from [s.buildable.libraries] *)
              Install.Entry.Sourced.create ~loc entry)
     else []
   in
@@ -672,8 +710,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
     let theories_deps =
       let scope = SC.find_scope_by_dir sctx dir in
       let coq_lib_db = Scope.coq_libs scope in
-      Resolve.of_result
-        (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories)
+      Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories
     in
     let theory_dirs = Path.Build.Set.empty in
     Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
@@ -701,16 +738,16 @@ let coqtop_args_extraction ~sctx ~dir ~dir_contents (s : Extraction.t) =
     let theories_deps =
       let scope = SC.find_scope_by_dir sctx dir in
       let coq_lib_db = Scope.coq_libs scope in
-      Resolve.of_result
-        (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories)
+      Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories
     in
     let theory_dirs = Path.Build.Set.empty in
     Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
       ~theory_dirs s.buildable
   in
-  let+ coq_module =
+  let* coq_module =
     let+ coq = Dir_contents.coq dir_contents in
     Coq_sources.extract coq s
   in
   let cctx = Context.for_module cctx coq_module in
-  (Context.coqc_file_flags cctx, cctx.boot_type)
+  let+ boot_type = Resolve.Memo.read_memo cctx.boot_type in
+  (Context.coqc_file_flags cctx, boot_type)
diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli
index dedd3108e903..157371123a3c 100644
--- a/src/dune_rules/coq_rules.mli
+++ b/src/dune_rules/coq_rules.mli
@@ -47,7 +47,7 @@ val setup_extraction_rules :
     build all dependencies of the Coq module [m]. *)
 val deps_of :
      dir:Path.Build.t
-  -> boot_type:Bootstrap.t
+  -> boot_type:Bootstrap.t Resolve.Memo.t
   -> Coq_module.t
   -> unit Dune_engine.Action_builder.t
 
diff --git a/src/dune_rules/scope.ml b/src/dune_rules/scope.ml
index 2577bc4778a4..858008f165b5 100644
--- a/src/dune_rules/scope.ml
+++ b/src/dune_rules/scope.ml
@@ -20,6 +20,33 @@ module DB = struct
 
   type t = { by_dir : scope Path.Source.Map.t }
 
+  let find_by_dir_in_map =
+    (* This function is linear in the depth of [dir] in the worst case, so if it
+       shows up in the profile we should memoize it. *)
+    let find_by_dir map (dir : Path.Source.t) =
+      let rec loop d =
+        match Path.Source.Map.find map d with
+        | Some s -> s
+        | None -> (
+          match Path.Source.parent d with
+          | Some d -> loop d
+          | None ->
+            Code_error.raise "find_by_dir: invalid directory"
+              [ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ])
+      in
+      loop dir
+    in
+    fun map dir ->
+      if Path.Build.is_root dir then
+        Code_error.raise "Scope.DB.find_by_dir_in_map got an invalid path"
+          [ ("dir", Path.Build.to_dyn dir) ];
+      find_by_dir map (Path.Build.drop_build_context_exn dir)
+
+  let find_by_dir t dir = find_by_dir_in_map t.by_dir dir
+
+  let find_by_project t project =
+    Path.Source.Map.find_exn t.by_dir (Dune_project.root project)
+
   module Found_or_redirect : sig
     type t = private
       | Found of Lib_info.external_
@@ -101,24 +128,6 @@ module DB = struct
       ~all:(fun () -> Lib_name.Map.keys map |> Memo.return)
       ~modules_of_lib ~lib_config
 
-  (* This function is linear in the depth of [dir] in the worst case, so if it
-     shows up in the profile we should memoize it. *)
-  let find_by_dir t (dir : Path.Source.t) =
-    let rec loop d =
-      match Path.Source.Map.find t.by_dir d with
-      | Some s -> s
-      | None -> (
-        match Path.Source.parent d with
-        | Some d -> loop d
-        | None ->
-          Code_error.raise "find_by_dir: invalid directory"
-            [ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ])
-    in
-    loop dir
-
-  let find_by_project t project =
-    Path.Source.Map.find_exn t.by_dir (Dune_project.root project)
-
   type redirect_to =
     | Project of Dune_project.t
     | Name of (Loc.t * Lib_name.t)
@@ -131,6 +140,11 @@ module DB = struct
       Lib.DB.Resolve_result.redirect (Some scope.db) (Loc.none, name)
     | Some (Name name) -> Lib.DB.Resolve_result.redirect None name
 
+  let public_theories ~find_db coq_stanzas =
+    List.filter_map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+        if Option.is_some stanza.package then Some (dir, stanza) else None)
+    |> Coq_lib.DB.create_from_coqlib_stanzas ~find_db ~parent:None
+
   (* Create a database from the public libraries defined in the stanzas *)
   let public_libs t ~installed_libs ~modules_of_lib ~lib_config stanzas =
     let public_libs =
@@ -174,8 +188,8 @@ module DB = struct
 
   module Path_source_map_traversals = Memo.Make_map_traversals (Path.Source.Map)
 
-  let scopes_by_dir context ~modules_of_lib ~projects ~public_libs stanzas
-      coq_stanzas =
+  let scopes_by_dir context ~modules_of_lib ~projects ~public_libs
+      ~public_theories stanzas coq_stanzas =
     let open Memo.O in
     let projects_by_dir =
       List.map projects ~f:(fun (project : Dune_project.t) ->
@@ -193,12 +207,11 @@ module DB = struct
           (Dune_project.root project, stanza))
       |> Path.Source.Map.of_list_multi
     in
-    let coq_db_by_project_dir =
-      List.map coq_stanzas ~f:(fun (dir, t) ->
-          let project = t.Coq_stanza.Theory.project in
-          (Dune_project.root project, (dir, t)))
+    let coq_stanzas_by_project_dir =
+      List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+          let project = stanza.project in
+          (Dune_project.root project, (dir, stanza)))
       |> Path.Source.Map.of_list_multi
-      |> Path.Source.Map.map ~f:Coq_lib.DB.create_from_coqlib_stanzas
     in
     let lib_config = Context.lib_config context in
     let+ db_by_project_dir =
@@ -215,14 +228,21 @@ module DB = struct
              in
              (project, db))
     in
+    let coq_db_by_project_dir =
+      let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in
+      Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir
+        ~f:(fun _dir project coq_stanzas ->
+          assert (Option.is_some project);
+          let stanzas = Option.value coq_stanzas ~default:[] in
+          Some stanzas)
+      |> Path.Source.Map.map ~f:(fun stanzas ->
+             Coq_lib.DB.create_from_coqlib_stanzas
+               ~parent:(Some public_theories) ~find_db stanzas)
+    in
     Path.Source.Map.merge db_by_project_dir coq_db_by_project_dir
       ~f:(fun _dir project_and_db coq_db ->
         let project, db = Option.value_exn project_and_db in
-        let coq_db =
-          match coq_db with
-          | Some db -> db
-          | None -> Coq_lib.DB.create_from_coqlib_stanzas []
-        in
+        let coq_db = Option.value_exn coq_db in
         let root =
           Path.Build.append_source context.build_dir (Dune_project.root project)
         in
@@ -236,20 +256,17 @@ module DB = struct
       let lib_config = Context.lib_config context in
       public_libs t ~installed_libs ~lib_config ~modules_of_lib stanzas
     in
+    let public_theories =
+      public_theories coq_stanzas ~find_db:(fun _ -> public_libs)
+    in
     let+ by_dir =
-      scopes_by_dir context ~projects ~public_libs ~modules_of_lib stanzas
-        coq_stanzas
+      scopes_by_dir context ~projects ~public_libs ~public_theories
+        ~modules_of_lib stanzas coq_stanzas
     in
     let value = { by_dir } in
     Fdecl.set t value;
     (value, public_libs)
 
-  let find_by_dir t dir =
-    if Path.Build.is_root dir then
-      Code_error.raise "Scope.DB.find_by_dir got an invalid path"
-        [ ("dir", Path.Build.to_dyn dir) ];
-    find_by_dir t (Path.Build.drop_build_context_exn dir)
-
   let create_from_stanzas ~projects ~context ~installed_libs ~modules_of_lib
       stanzas =
     let stanzas, coq_stanzas =
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/cboot.opam b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/A.opam
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-boot.t/cboot.opam
rename to test/blackbox-tests/test-cases/coq/compose-boot.t/A/A.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v
new file mode 100644
index 000000000000..8089bf38ce4c
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v
@@ -0,0 +1 @@
+Inductive AnotherBegining := Of | The | Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune
new file mode 100644
index 000000000000..c5888866aadd
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name A)
+ (package A)
+ (boot))
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-boot.t/dune-project
rename to test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/ccycle.opam b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/B.opam
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/ccycle.opam
rename to test/blackbox-tests/test-cases/coq/compose-boot.t/B/B.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v
new file mode 100644
index 000000000000..46e4b397d40e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v
@@ -0,0 +1 @@
+Inductive Begining := Of | The | Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune
new file mode 100644
index 000000000000..128896380043
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name B)
+ (package B)
+ (boot))
+
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project
new file mode 100644
index 000000000000..9ef6b81a34a1
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.5)
+
+(using coq 0.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v
deleted file mode 100644
index eaaf0e55b2cf..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v
+++ /dev/null
@@ -1 +0,0 @@
-Definition id := forall (X : Type), X.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/dune
deleted file mode 100644
index cb370c83b613..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/dune
+++ /dev/null
@@ -1,7 +0,0 @@
-(coq.theory
- (name Coq)
- (package cboot)
- (boot))
-
-(include_subdirs qualified)
-
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune
deleted file mode 100644
index 32d3fd982714..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(rule
- (alias default)
- (action (echo "%{read:cboot.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace
new file mode 100644
index 000000000000..0c226b5b0c6e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t
index 8f2f58e436b1..a7d7a27e307e 100644
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t
@@ -1,2 +1,7 @@
-# Test only works on Coq 8.12 due to boot constraints
-# $ dune build --display short --debug-dependency-path
+Testing composition with two boot libraries
+
+  $ dune build
+  Error: Cannot have more than one boot theory in scope:
+  - B at B/dune:1
+  - A at A/dune:1
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune
deleted file mode 100644
index 5402df7cc246..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(coq.theory
- (name user)
- (package cboot))
-
-
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v
deleted file mode 100644
index cdda78d422b5..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v
+++ /dev/null
@@ -1 +0,0 @@
-Definition a := id.
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/a.v
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/a/a.v
rename to test/blackbox-tests/test-cases/coq/compose-cycle.t/A/a.v
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune
new file mode 100644
index 000000000000..90fefd9be0ec
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A)
+ (theories B))
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/b.v
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/b/b.v
rename to test/blackbox-tests/test-cases/coq/compose-cycle.t/B/b.v
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune
new file mode 100644
index 000000000000..f087163ebd4d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune
deleted file mode 100644
index 478550e09852..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(coq.theory
- (name a)
- (package ccycle)
- (theories b))
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune
deleted file mode 100644
index 5f42b4087e99..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(coq.theory
- (name b)
- (package ccycle)
- (theories a))
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune
deleted file mode 100644
index e622b2ade9e6..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(rule
- (alias default)
- (action (echo "%{read:ccycle.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project
index 9ef6b81a34a1..06314b536ad9 100644
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project
+++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project
@@ -1,3 +1,2 @@
-(lang dune 2.5)
-
-(using coq 0.2)
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
index 1934679769f2..6a76d25981bd 100644
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
@@ -1,28 +1,11 @@
-  $ dune build --debug-dependency-path
-  File "a/dune", line 2, characters 7-8:
-  2 |  (name a)
-             ^
-  Error: Cycle found
-  - b
-  - a
-  - b
-  -> required by _build/default/a/a.v.d
-  -> required by _build/default/a/a.vo
-  -> required by _build/install/default/lib/coq/user-contrib/a/a.vo
-  -> required by _build/default/ccycle.install
-  -> required by %{read:ccycle.install} at dune:3
-  -> required by alias default in dune:1
-  File "b/dune", line 2, characters 7-8:
-  2 |  (name b)
-             ^
-  Error: Cycle found
-  - a
-  - b
-  - a
-  -> required by _build/default/b/b.v.d
-  -> required by _build/default/b/b.vo
-  -> required by _build/install/default/lib/coq/user-contrib/b/b.vo
-  -> required by _build/default/ccycle.install
-  -> required by %{read:ccycle.install} at dune:3
-  -> required by alias default in dune:1
+We check cycles are detected
+  $ dune build
+  Error: Dependency cycle between:
+     theory A in A
+  -> theory B in B
+  -> theory A in A
+  -> required by _build/default/A/a.v.d
+  -> required by _build/default/A/.a.aux
+  -> required by alias A/all
+  -> required by alias default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v
new file mode 100644
index 000000000000..f1904cefbfc8
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v
@@ -0,0 +1,2 @@
+From B Require Import b.
+Print message.
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune
new file mode 100644
index 000000000000..90fefd9be0ec
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A)
+ (theories B))
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
new file mode 100644
index 000000000000..361fdc9d64d5
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
@@ -0,0 +1,20 @@
+We test composing a project with an installed Coq theory. The installed theory
+does *not* have to be a dune project.
+
+  $ export COQLIB=.
+
+TODO: Currently this is not supported so the output is garbage
+
+  $ cd A
+  $ dune build
+  File "dune", line 3, characters 11-12:
+  3 |  (theories B))
+                 ^
+  Theory B not found
+  -> required by theory A in .
+  -> required by _build/default/a.v.d
+  -> required by _build/default/.a.aux
+  -> required by alias all
+  -> required by alias default
+  [1]
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v b/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v
new file mode 100644
index 000000000000..54ff44b1c610
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v
@@ -0,0 +1,3 @@
+From Coq Require Import String.
+Local Open Scope string_scope.
+Definition message := "Hello from an install location!".
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/csimple.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/A.opam
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-simple.t/csimple.opam
rename to test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/A.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v
new file mode 100644
index 000000000000..ebbd6bd3ea04
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v
@@ -0,0 +1,3 @@
+From Coq Require Import String.
+Local Open Scope string_scope.
+Definition message := "I am the the private A ".
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune
new file mode 100644
index 000000000000..dc6e6bf392b4
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/subtheory.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/A.opam
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-sub-theory.t/subtheory.opam
rename to test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/A.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v
new file mode 100644
index 000000000000..01c353dd662e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v
@@ -0,0 +1,3 @@
+From Coq Require Import String.
+Local Open Scope string_scope.
+Definition message := "I am the vendored A".
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune
new file mode 100644
index 000000000000..084e1edeb448
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name A)
+ (package A))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v
new file mode 100644
index 000000000000..daa1e640ee1b
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v
@@ -0,0 +1,7 @@
+From Coq Require Import String.
+From A Require Import a.
+
+Local Open Scope string_scope.
+
+Print message.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune
new file mode 100644
index 000000000000..f087163ebd4d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v
new file mode 100644
index 000000000000..daa1e640ee1b
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v
@@ -0,0 +1,7 @@
+From Coq Require Import String.
+From A Require Import a.
+
+Local Open Scope string_scope.
+
+Print message.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune
new file mode 100644
index 000000000000..036c18c2a371
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name C)
+ (package C)
+ (theories A))
+
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t
new file mode 100644
index 000000000000..cc55f34adfdb
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t
@@ -0,0 +1,16 @@
+We have two theories, A and A_vendored both called A. We test which one a
+private plugin B and the public package C will pick up.
+
+B will pick up the private one:
+  $ dune build B
+  message = "I am the the private A "
+       : string
+
+C picks up the private one too:
+  $ dune build C
+  File "C/dune", line 4, characters 11-12:
+  4 |  (theories A))
+                 ^
+  Theory "A" is private, it cannot be a dependency of a public theory. You need
+  to associate "A" to a package.
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-private.t/A/A.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v
new file mode 100644
index 000000000000..831752c569d8
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v
@@ -0,0 +1,2 @@
+
+Inductive Hello := World | Bye.
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune
new file mode 100644
index 000000000000..dc6e6bf392b4
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v
new file mode 100644
index 000000000000..5659f2682e6d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v
@@ -0,0 +1,4 @@
+From A Require Import a.
+
+Check Hello.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune
new file mode 100644
index 000000000000..f087163ebd4d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C.opam b/test/blackbox-tests/test-cases/coq/compose-private.t/C.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-private.t/C/c.v
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune
new file mode 100644
index 000000000000..6ddaa5c1f9a9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name C)
+ (package C)
+ (theories B))
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private.t/run.t
new file mode 100644
index 000000000000..02db95b3c18a
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-private.t/run.t
@@ -0,0 +1,13 @@
+Testing composition of theories with two private theories and a third public
+theory. As expected, the private theories build, but the public theory fails
+because a public theory cannot depend on a private theory. 
+
+  $ dune build
+  Hello
+       : Set
+  File "C/dune", line 4, characters 11-12:
+  4 |  (theories B))
+                 ^
+  Theory "B" is private, it cannot be a dependency of a public theory. You need
+  to associate "B" to a package.
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/A.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v
new file mode 100644
index 000000000000..92d80e770f16
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v
@@ -0,0 +1,3 @@
+From C Require Import c.
+
+Inductive Hello := World | Bye.
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune
new file mode 100644
index 000000000000..f8bc0053ff65
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name A)
+ (package A)
+ (theories C))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/B.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v
new file mode 100644
index 000000000000..5659f2682e6d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v
@@ -0,0 +1,4 @@
+From A Require Import a.
+
+Check Hello.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune
new file mode 100644
index 000000000000..d421f8800b5a
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (package B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/C.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/C.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v
new file mode 100644
index 000000000000..b68952f12fa6
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v
@@ -0,0 +1 @@
+From B Require Import b.
\ No newline at end of file
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune
new file mode 100644
index 000000000000..292624eb16d3
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name C)
+ (package C)
+ (theories B))
\ No newline at end of file
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace
new file mode 100644
index 000000000000..0c226b5b0c6e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
new file mode 100644
index 000000000000..acf813e8090d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
@@ -0,0 +1,38 @@
+Testing composition of theories accross a dune workspace with cyclic
+dependencies.
+
+  $ dune build A
+  Error: Dependency cycle between:
+     theory A in A
+  -> theory B in B
+  -> theory C in C
+  -> theory A in A
+  -> required by _build/default/A/a.v.d
+  -> required by _build/default/A/.a.aux
+  -> required by alias A/all
+  -> required by alias A/default
+  [1]
+
+  $ dune build B
+  Error: Dependency cycle between:
+     theory B in B
+  -> theory C in C
+  -> theory A in A
+  -> theory B in B
+  -> required by _build/default/B/b.v.d
+  -> required by _build/default/B/.b.aux
+  -> required by alias B/all
+  -> required by alias B/default
+  [1]
+
+  $ dune build C
+  Error: Dependency cycle between:
+     theory C in C
+  -> theory A in A
+  -> theory B in B
+  -> theory C in C
+  -> required by _build/default/C/c.v.d
+  -> required by _build/default/C/.c.aux
+  -> required by alias C/all
+  -> required by alias C/default
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/A.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v
new file mode 100644
index 000000000000..831752c569d8
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v
@@ -0,0 +1,2 @@
+
+Inductive Hello := World | Bye.
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune
new file mode 100644
index 000000000000..dc6e6bf392b4
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/B.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v
new file mode 100644
index 000000000000..5659f2682e6d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v
@@ -0,0 +1,4 @@
+From A Require Import a.
+
+Check Hello.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune
new file mode 100644
index 000000000000..d421f8800b5a
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (package B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/C.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/C.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v
new file mode 100644
index 000000000000..c4484984fbef
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v
@@ -0,0 +1,2 @@
+
+Check bye.
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune
new file mode 100644
index 000000000000..292624eb16d3
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name C)
+ (package C)
+ (theories B))
\ No newline at end of file
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace
new file mode 100644
index 000000000000..0c226b5b0c6e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
new file mode 100644
index 000000000000..61d86ca1a84f
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
@@ -0,0 +1,15 @@
+Testing composition of theories accross a dune workspace with a missing
+dependency.
+
+  $ dune build C
+  File "B/dune", line 4, characters 11-12:
+  4 |  (theories A))
+                 ^
+  Theory A not found
+  -> required by theory B in B
+  -> required by theory C in C
+  -> required by _build/default/C/c.v.d
+  -> required by _build/default/C/.c.aux
+  -> required by alias C/all
+  -> required by alias C/default
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/A.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v
new file mode 100644
index 000000000000..831752c569d8
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v
@@ -0,0 +1,2 @@
+
+Inductive Hello := World | Bye.
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune
new file mode 100644
index 000000000000..084e1edeb448
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name A)
+ (package A))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v
new file mode 100644
index 000000000000..5659f2682e6d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v
@@ -0,0 +1,4 @@
+From A Require Import a.
+
+Check Hello.
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune
new file mode 100644
index 000000000000..f087163ebd4d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace
new file mode 100644
index 000000000000..0c226b5b0c6e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t
new file mode 100644
index 000000000000..22e411a63e87
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t
@@ -0,0 +1,28 @@
+Testing composition of theories accross a dune workspace
+
+  $ dune build B
+  Hello
+       : Set
+
+Inspecting the build directory
+  $ find _build/default
+  _build/default
+  _build/default/B
+  _build/default/B/b.vok
+  _build/default/B/b.v
+  _build/default/B/b.glob
+  _build/default/B/b.vos
+  _build/default/B/b.v.d
+  _build/default/B/b.vo
+  _build/default/B/.b.aux
+  _build/default/A
+  _build/default/A/a.vok
+  _build/default/A/a.v
+  _build/default/A/.a.aux
+  _build/default/A/a.vo
+  _build/default/A/a.glob
+  _build/default/A/a.v.d
+  _build/default/A/a.vos
+  _build/default/.dune
+  _build/default/.dune/configurator.v2
+  _build/default/.dune/configurator
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-self.t/A/a.v
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune
new file mode 100644
index 000000000000..d44a666925a7
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project
new file mode 100644
index 000000000000..06314b536ad9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
new file mode 100644
index 000000000000..3bb751183049
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
@@ -0,0 +1,9 @@
+Composing a theory with itself should cause a cycle
+  $ dune build
+  Error: Dependency cycle between:
+     theory A in A
+  -> required by _build/default/A/a.v.d
+  -> required by _build/default/A/.a.aux
+  -> required by alias A/all
+  -> required by alias default
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/a.v
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-simple.t/a/a.v
rename to test/blackbox-tests/test-cases/coq/compose-simple.t/A/a.v
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune
new file mode 100644
index 000000000000..86ee2ef8f61e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name A)
+ (package Simple))
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v
similarity index 50%
rename from test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v
rename to test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v
index e184683b4d42..951f7a4ee5ef 100644
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v
@@ -1,3 +1,3 @@
-From a Require Import a.
+From A Require Import a.
 
 Definition bar := a.foo.
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune
new file mode 100644
index 000000000000..7893d7c9e63e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (package Simple)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/Simple.opam b/test/blackbox-tests/test-cases/coq/compose-simple.t/Simple.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune
deleted file mode 100644
index 099b8f56a24d..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(coq.theory
- (name a)
- (package csimple))
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune
deleted file mode 100644
index e4edf23190e7..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(coq.theory
- (name b)
- (package csimple)
- (theories a))
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune
deleted file mode 100644
index f7a7db897dbd..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(rule
- (alias default)
- (action (echo "%{read:csimple.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project
index 9ef6b81a34a1..06314b536ad9 100644
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project
@@ -1,3 +1,2 @@
-(lang dune 2.5)
-
-(using coq 0.2)
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
index d1626e74578f..205ce1ae3500 100644
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
@@ -1,16 +1,32 @@
-  $ dune build --display short --debug-dependency-path
-        coqdep a/a.v.d
-        coqdep b/b.v.d
-          coqc a/.a.aux,a/a.{glob,vo}
-          coqc b/.b.aux,b/b.{glob,vo}
-  lib: [
-    "_build/install/default/lib/csimple/META"
-    "_build/install/default/lib/csimple/dune-package"
-    "_build/install/default/lib/csimple/opam"
-  ]
-  lib_root: [
-    "_build/install/default/lib/coq/user-contrib/a/a.v" {"coq/user-contrib/a/a.v"}
-    "_build/install/default/lib/coq/user-contrib/a/a.vo" {"coq/user-contrib/a/a.vo"}
-    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
-    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
-  ]
+Testing a simple composition of theories. We have two theories A and B and B
+depends on A.
+
+  $ dune build
+
+We inspect the contents of the build directory.
+
+  $ find _build/default
+  _build/default
+  _build/default/META.Simple
+  _build/default/B
+  _build/default/B/b.vok
+  _build/default/B/b.v
+  _build/default/B/b.glob
+  _build/default/B/b.vos
+  _build/default/B/b.v.d
+  _build/default/B/b.vo
+  _build/default/B/.b.aux
+  _build/default/Simple.dune-package
+  _build/default/Simple.install
+  _build/default/A
+  _build/default/A/a.vok
+  _build/default/A/a.v
+  _build/default/A/.a.aux
+  _build/default/A/a.vo
+  _build/default/A/a.glob
+  _build/default/A/a.v.d
+  _build/default/A/a.vos
+  _build/default/Simple.opam
+  _build/default/.dune
+  _build/default/.dune/configurator.v2
+  _build/default/.dune/configurator
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/a.v
similarity index 100%
rename from test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/a.v
rename to test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/a.v
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune
new file mode 100644
index 000000000000..237bfa399e64
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune
@@ -0,0 +1,3 @@
+(coq.theory
+ (name Foo.A)
+ (package Subtheory))
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v
new file mode 100644
index 000000000000..1379965e9ff3
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v
@@ -0,0 +1,3 @@
+From Foo Require Import a.
+
+Definition bar := a.foo.
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune
new file mode 100644
index 000000000000..d2d6fca00241
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (package Subtheory)
+ (theories Foo.A))
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/Subtheory.opam b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/Subtheory.opam
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune
deleted file mode 100644
index d34c322f227e..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(coq.theory
- (name foo.a)
- (package subtheory))
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v
deleted file mode 100644
index fc1eff1cce39..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v
+++ /dev/null
@@ -1,3 +0,0 @@
-From foo Require Import a.
-
-Definition bar := a.foo.
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune
deleted file mode 100644
index 3ed0a09517cd..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(coq.theory
- (name b)
- (package subtheory)
- (theories foo.a))
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune
deleted file mode 100644
index 5ee910867dec..000000000000
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(rule
- (alias default)
- (action (echo "%{read:subtheory.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project
index d18101b40de2..06314b536ad9 100644
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project
@@ -1,2 +1,2 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
index 8f1321b1291c..0e7d74ed9832 100644
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
@@ -1,16 +1,52 @@
-  $ dune build --display short --debug-dependency-path
-        coqdep b/b.v.d
-        coqdep a/a.v.d
-          coqc a/.a.aux,a/a.{glob,vo}
-          coqc b/.b.aux,b/b.{glob,vo}
-  lib: [
-    "_build/install/default/lib/subtheory/META"
-    "_build/install/default/lib/subtheory/dune-package"
-    "_build/install/default/lib/subtheory/opam"
-  ]
-  lib_root: [
-    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
-    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
-    "_build/install/default/lib/coq/user-contrib/foo/a/a.v" {"coq/user-contrib/foo/a/a.v"}
-    "_build/install/default/lib/coq/user-contrib/foo/a/a.vo" {"coq/user-contrib/foo/a/a.vo"}
-  ]
+Testing dependencies on subtheories. We have two theories A and B, but A is
+defined as Foo.A. This changes the install layout of A.
+
+  $ dune build
+
+Inspecting the build and install directory
+  $ find _build/
+  _build/
+  _build/.db
+  _build/.filesystem-clock
+  _build/.digest-db
+  _build/install
+  _build/install/default
+  _build/install/default/lib
+  _build/install/default/lib/Subtheory
+  _build/install/default/lib/Subtheory/dune-package
+  _build/install/default/lib/Subtheory/META
+  _build/install/default/lib/Subtheory/opam
+  _build/install/default/lib/coq
+  _build/install/default/lib/coq/user-contrib
+  _build/install/default/lib/coq/user-contrib/B
+  _build/install/default/lib/coq/user-contrib/B/b.v
+  _build/install/default/lib/coq/user-contrib/B/b.vo
+  _build/install/default/lib/coq/user-contrib/Foo
+  _build/install/default/lib/coq/user-contrib/Foo/A
+  _build/install/default/lib/coq/user-contrib/Foo/A/a.v
+  _build/install/default/lib/coq/user-contrib/Foo/A/a.vo
+  _build/default
+  _build/default/B
+  _build/default/B/b.vok
+  _build/default/B/b.v
+  _build/default/B/b.glob
+  _build/default/B/b.vos
+  _build/default/B/b.v.d
+  _build/default/B/b.vo
+  _build/default/B/.b.aux
+  _build/default/META.Subtheory
+  _build/default/Subtheory.dune-package
+  _build/default/A
+  _build/default/A/a.vok
+  _build/default/A/a.v
+  _build/default/A/.a.aux
+  _build/default/A/a.vo
+  _build/default/A/a.glob
+  _build/default/A/a.v.d
+  _build/default/A/a.vos
+  _build/default/Subtheory.install
+  _build/default/Subtheory.opam
+  _build/default/.dune
+  _build/default/.dune/configurator.v2
+  _build/default/.dune/configurator
+  _build/log
diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t
index 0285fd613ea8..d47473520f3c 100644
--- a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t
@@ -1,12 +1,11 @@
-  $ dune build --debug-dependency-path
-  File "b/dune", line 4, characters 11-12:
-  4 |  (theories a))
-                 ^
-  Error: Theory a not found
-  -> required by _build/default/b/b.v.d
-  -> required by _build/default/b/b.vo
-  -> required by _build/install/default/lib/coq/user-contrib/b/b.vo
-  -> required by _build/default/cvendor.install
-  -> required by %{read:cvendor.install} at dune:3
-  -> required by alias default in dune:1
-  [1]
+
+  $ dune build
+  lib: [
+    "_build/install/default/lib/cvendor/META"
+    "_build/install/default/lib/cvendor/dune-package"
+    "_build/install/default/lib/cvendor/opam"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
+    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
+  ]
diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t
index 09dac49026d7..785e823b623a 100644
--- a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t
@@ -2,8 +2,9 @@
   File "public/dune", line 4, characters 11-18:
   4 |  (theories private))
                  ^^^^^^^
-  Error: Theory "private" is private, it cannot be a dependency of a public
-  theory. You need to associate "private" to a package.
+  Theory "private" is private, it cannot be a dependency of a public theory.
+  You need to associate "private" to a package.
+  -> required by theory public in public
   -> required by _build/default/public/b.v.d
   -> required by _build/default/public/b.vo
   -> required by _build/install/default/lib/coq/user-contrib/public/b.vo