diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
index c3eb5a75ddbe..f86aa74aff65 100644
--- a/src/dune_rules/coq_lib.ml
+++ b/src/dune_rules/coq_lib.ml
@@ -70,7 +70,7 @@ module Error = struct
   let annots =
     User_message.Annots.singleton User_message.Annots.needs_stack_trace ()
 
-  let duplicate_theory_name (loc, name) =
+  let duplicate_theory_name ~loc name =
     let name = Coq_lib_name.to_string name in
     User_error.raise ~loc [ Pp.textf "Duplicate theory name: %s" name ]
 
@@ -111,7 +111,7 @@ module Error = struct
   let duplicate_boot_lib theories =
     let open Coq_stanza.Theory in
     let name (t : Coq_stanza.Theory.t) =
-      let name = Coq_lib_name.to_string (snd t.name) in
+      let name = Coq_lib_name.to_string t.name in
       Pp.textf "%s at %s" name (Loc.to_file_colon_line t.buildable.loc)
     in
     User_error.raise
@@ -150,8 +150,9 @@ module DB = struct
   module rec R : sig
     val resolve :
          t
+      -> loc:Loc.t
       -> coq_lang_version:Dune_sexp.Syntax.Version.t
-      -> Loc.t * Coq_lib_name.t
+      -> Coq_lib_name.t
       -> lib Resolve.Memo.t
   end = struct
     open R
@@ -167,7 +168,7 @@ module DB = struct
 
     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 id = Id.create ~path:dir ~name:s.name in
         let coq_lang_version = s.buildable.coq_lang_version in
         let open Memo.O in
         let* boot = if s.boot then Resolve.Memo.return None else boot coq_db in
@@ -193,7 +194,7 @@ module DB = struct
                          [ Pp.textf
                              "private theory %s may not depend on a public \
                               library"
-                             (Coq_lib_name.to_string (snd s.name))
+                             (Coq_lib_name.to_string s.name)
                          ]
               in
               (loc, lib))
@@ -214,7 +215,7 @@ module DB = struct
           in
           Resolve.Memo.List.map s.buildable.theories ~f:(fun (loc, theory) ->
               let open Resolve.Memo.O in
-              let* theory = resolve ~coq_lang_version coq_db (loc, theory) in
+              let* theory = resolve ~coq_lang_version coq_db ~loc theory in
               let* () = Resolve.Memo.lift @@ check_boot theory in
               let+ () =
                 if allow_private_deps then Resolve.Memo.return ()
@@ -244,7 +245,7 @@ module DB = struct
         let theories = map_error theories in
         let libraries = map_error libraries in
 
-        { loc = fst s.name
+        { loc = s.loc
         ; boot
         ; id
         ; implicit = s.boot
@@ -275,23 +276,23 @@ module DB = struct
       let memo =
         Memo.create "create-from-stanza"
           ~human_readable_description:(fun (_, _, path, theory) ->
-            Id.pp (Id.create ~path ~name:(snd theory.name)))
+            Id.pp (Id.create ~path ~name: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) =
+    let rec find coq_db name =
       match coq_db.resolve name with
       | `Theory (db, dir, stanza) -> Some (db, dir, stanza)
-      | `Redirect coq_db -> find coq_db (loc, name)
+      | `Redirect coq_db -> find coq_db name
       | `Not_found -> (
         match coq_db.parent with
         | None -> None
-        | Some parent -> find parent (loc, name))
+        | Some parent -> find parent name)
 
-    let find coq_db ~coq_lang_version (loc, name) =
-      match find coq_db (loc, name) with
+    let find coq_db ~coq_lang_version name =
+      match find coq_db name with
       | None -> `Not_found
       | Some (mldb, dir, stanza) when coq_lang_version >= (0, 4) ->
         `Found (mldb, dir, stanza)
@@ -300,8 +301,8 @@ module DB = struct
         | `Not_found -> `Hidden
         | `Theory _ | `Redirect _ -> `Found (mldb, dir, stanza))
 
-    let resolve coq_db ~coq_lang_version (loc, name) =
-      match find coq_db ~coq_lang_version (loc, name) with
+    let resolve coq_db ~loc ~coq_lang_version name =
+      match find coq_db ~coq_lang_version name with
       | `Not_found -> Error.theory_not_found ~loc name
       | `Hidden -> Error.hidden_without_composition ~loc name
       | `Found (db, dir, stanza) ->
@@ -344,8 +345,7 @@ module DB = struct
         with
         | [] -> None
         | [ ((theory : Coq_stanza.Theory.t), _entry) ] ->
-          let loc, name = theory.name in
-          Some (loc, name, theory.buildable.coq_lang_version)
+          Some (theory.loc, theory.name, theory.buildable.coq_lang_version)
         | boots ->
           let stanzas = List.map boots ~f:fst in
           Error.duplicate_boot_lib stanzas
@@ -356,7 +356,7 @@ module DB = struct
         let lib =
           Memo.lazy_ (fun () ->
               let t = Fdecl.get t in
-              resolve t ~coq_lang_version (loc, name))
+              resolve t ~coq_lang_version ~loc name)
         in
         Some (loc, lib)
     in
@@ -365,11 +365,11 @@ module DB = struct
         match
           Coq_lib_name.Map.of_list_map entries
             ~f:(fun ((theory : Coq_stanza.Theory.t), entry) ->
-              (snd theory.name, (theory, entry)))
+              (theory.name, (theory, entry)))
         with
         | Ok m -> m
         | Error (_name, _, (theory, _entry)) ->
-          Error.duplicate_theory_name theory.name
+          Error.duplicate_theory_name ~loc:theory.loc theory.name
       in
       fun name ->
         match Coq_lib_name.Map.find map name with
@@ -382,18 +382,19 @@ module DB = struct
     Fdecl.set t { boot; resolve; parent };
     Fdecl.get t
 
-  let find_many t ~loc theories ~coq_lang_version =
-    Resolve.Memo.List.map theories ~f:(fun name ->
-        resolve ~coq_lang_version t (loc, name))
+  let find_many t theories ~coq_lang_version =
+    Resolve.Memo.List.map theories ~f:(fun (loc, name) ->
+        resolve ~coq_lang_version t ~loc name)
 
   let requires_for_user_written db theories ~coq_lang_version =
     let open Memo.O in
     let+ theories =
-      Resolve.Memo.List.map theories ~f:(resolve ~coq_lang_version db)
+      Resolve.Memo.List.map theories ~f:(fun (loc, name) ->
+          resolve ~coq_lang_version db ~loc name)
     in
     Resolve.O.(theories >>= top_closure)
 
-  let resolve db l ~coq_lang_version = resolve db ~coq_lang_version l
+  let resolve db ~loc l ~coq_lang_version = resolve db ~loc ~coq_lang_version l
 end
 
 let theories_closure t = Lazy.force t.theories_closure
diff --git a/src/dune_rules/coq_lib.mli b/src/dune_rules/coq_lib.mli
index 062a241733df..3bd47e6cdd06 100644
--- a/src/dune_rules/coq_lib.mli
+++ b/src/dune_rules/coq_lib.mli
@@ -39,8 +39,7 @@ module DB : sig
 
   val find_many :
        t
-    -> loc:Loc.t
-    -> Coq_lib_name.t list
+    -> (Loc.t * Coq_lib_name.t) list
     -> coq_lang_version:Dune_sexp.Syntax.Version.t
     -> lib list Resolve.Memo.t
 
@@ -48,7 +47,8 @@ module DB : sig
 
   val resolve :
        t
-    -> Loc.t * Coq_lib_name.t
+    -> loc:Loc.t
+    -> Coq_lib_name.t
     -> coq_lang_version:Dune_sexp.Syntax.Version.t
     -> lib Resolve.Memo.t
 
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 290ccf0373c2..51716c2b61c8 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -442,13 +442,14 @@ module Coqdoc_mode = struct
 end
 
 let coqdoc_directory_targets ~dir:obj_dir (theory : Coq_stanza.Theory.t) =
-  let loc, name = theory.name in
+  let loc = theory.loc in
+  let name = theory.name in
   Path.Build.Map.of_list_exn
     [ (Coqdoc_mode.directory Html obj_dir name, loc)
     ; (Coqdoc_mode.directory Latex obj_dir name, loc)
     ]
 
-let coqdoc_rule (cctx : _ Context.t) ~sctx ~name:(_, name) ~file_flags ~mode
+let coqdoc_rule (cctx : _ Context.t) ~sctx ~name ~file_flags ~mode
     ~theories_deps coq_modules =
   let obj_dir = cctx.dir in
   let doc_dir = Coqdoc_mode.directory mode obj_dir name in
@@ -533,12 +534,12 @@ let source_rule ~sctx theories =
     List.concat l |> List.rev_map ~f:(fun m -> Path.build (Coq_module.source m)))
 
 let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
-  let name = snd s.name in
+  let name = 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 ~coq_lang_version:s.buildable.coq_lang_version
-      s.name
+      ~loc:s.loc s.name
   in
   let* coq_dir_contents = Dir_contents.coq dir_contents in
   let* cctx =
@@ -589,11 +590,11 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   |> Super_context.add_rules ~loc ~dir sctx
 
 let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
-  let name = snd s.name in
+  let name = 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
+    Coq_lib.DB.resolve coq_lib_db ~loc:s.loc s.name
       ~coq_lang_version:s.buildable.coq_lang_version
   in
   let* coq_dir_contents = Dir_contents.coq dir_contents in
@@ -656,9 +657,9 @@ let install_rules ~sctx ~dir s =
     let loc = s.buildable.loc in
     let scope = SC.find_scope_by_dir sctx dir in
     let* dir_contents = Dir_contents.get sctx ~dir in
-    let name = snd s.name in
+    let name = s.name in
     (* This must match the wrapper prefix for now to remain compatible *)
-    let dst_suffix = Coq_lib_name.dir (snd s.name) in
+    let dst_suffix = Coq_lib_name.dir s.name in
     (* These are the rules for now, coq lang 2.0 will make this uniform *)
     let dst_dir =
       if s.boot then
diff --git a/src/dune_rules/coq_sources.ml b/src/dune_rules/coq_sources.ml
index a11a0d641dbc..31d18943296d 100644
--- a/src/dune_rules/coq_sources.ml
+++ b/src/dune_rules/coq_sources.ml
@@ -63,12 +63,10 @@ let of_dir stanzas ~dir ~include_subdirs ~dirs =
     | Theory.T coq ->
       let modules = Coq_module.eval ~dir coq.modules ~standard:modules in
       let directories =
-        Coq_lib_name.Map.add_exn acc.directories (snd coq.name)
+        Coq_lib_name.Map.add_exn acc.directories coq.name
           (List.map dirs ~f:(fun (d, _, _) -> d))
       in
-      let libraries =
-        Coq_lib_name.Map.add_exn acc.libraries (snd coq.name) modules
-      in
+      let libraries = Coq_lib_name.Map.add_exn acc.libraries coq.name modules in
       let rev_map =
         List.fold_left modules ~init:acc.rev_map ~f:(fun acc m ->
             Coq_module.Map.add_exn acc m (`Theory coq))
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index a0db88f983a4..93de0b1beda3 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/src/dune_rules/coq_stanza.ml
@@ -84,7 +84,8 @@ end
 
 module Theory = struct
   type t =
-    { name : Loc.t * Coq_lib_name.t
+    { loc : Loc.t
+    ; name : Coq_lib_name.t
     ; package : Package.t option
     ; project : Dune_project.t
     ; synopsis : string option
@@ -134,7 +135,7 @@ module Theory = struct
 
   let decode =
     fields
-      (let+ name = field "name" Coq_lib_name.decode
+      (let+ loc, name = field "name" Coq_lib_name.decode
        and+ package = field_o "package" Stanza_common.Pkg.decode
        and+ project = Dune_project.get_exn ()
        and+ public = coq_public_decode
@@ -145,7 +146,8 @@ module Theory = struct
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode in
        let package = select_deprecation ~package ~public in
-       { name
+       { loc
+       ; name
        ; package
        ; project
        ; synopsis
diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli
index e6f2b9186a8d..fc70a86cdec4 100644
--- a/src/dune_rules/coq_stanza.mli
+++ b/src/dune_rules/coq_stanza.mli
@@ -25,7 +25,8 @@ end
 
 module Theory : sig
   type t =
-    { name : Loc.t * Coq_lib_name.t
+    { loc : Loc.t
+    ; name : Coq_lib_name.t
     ; package : Package.t option
     ; project : Dune_project.t
     ; synopsis : string option