diff --git a/CHANGES.md b/CHANGES.md
index e23f5b1fd851..7304ba211dfd 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,7 @@ Unreleased
 
 - Fix preludes not being recorded as dependencies in the `(mdx)` stanza (#7109,
   fixes #7077, @emillon).
+- Make coq_db creation in scope lazy (@ejgallego, #)
 
 3.7.0 (2023-02-17)
 ------------------
diff --git a/src/dune_rules/scope.ml b/src/dune_rules/scope.ml
index 4da8b1e55096..f41b3829449d 100644
--- a/src/dune_rules/scope.ml
+++ b/src/dune_rules/scope.ml
@@ -4,7 +4,7 @@ open Memo.O
 type t =
   { project : Dune_project.t
   ; db : Lib.DB.t
-  ; coq_db : Coq_lib.DB.t
+  ; coq_db : Coq_lib.DB.t Lazy.t
   ; root : Path.Build.t
   }
 
@@ -14,7 +14,7 @@ let project t = t.project
 
 let libs t = t.db
 
-let coq_libs t = t.coq_db
+let coq_libs t = Lazy.force t.coq_db
 
 module DB = struct
   type scope = t
@@ -154,13 +154,16 @@ 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 =
+  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 (stanza, Coq_lib.DB.Theory dir)
         else None)
     |> Coq_lib.DB.create_from_coqlib_stanzas ~find_db ~parent:None
 
+  let public_theories ~find_db coq_stanzas =
+    Lazy.from_fun (public_theories ~find_db coq_stanzas)
+
   (* Create a database from the public libraries defined in the stanzas *)
   let public_libs t ~installed_libs ~lib_config stanzas =
     let public_libs =
@@ -265,14 +268,16 @@ module DB = struct
                 let entry =
                   match stanza.package with
                   | None -> Coq_lib.DB.Theory dir
-                  | Some _ -> Redirect public_theories
+                  | Some _ -> Redirect (Lazy.force public_theories)
                 in
                 (stanza, entry))
           in
           Some entries)
       |> Path.Source.Map.map ~f:(fun stanzas ->
-             Coq_lib.DB.create_from_coqlib_stanzas
-               ~parent:(Some public_theories) ~find_db stanzas)
+             Lazy.from_fun (fun () ->
+                 let public_theories = Lazy.force public_theories in
+                 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 ->