diff --git a/CHANGES.md b/CHANGES.md
index 4abcb21aa9b..acbe005cc7a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -9,6 +9,12 @@ Unreleased
 
 - Support new locations of unix, str, dynlink in OCaml >= 5.0 (#5582, @dra27)
 
+- The ``coq.theory`` stanza now produces rules for running ``coqdoc``. Given a
+  theory named ``mytheory``, the directory targets ``mytheory.html/`` and
+  ``mytheory.tex/`` or additionally the aliases `@doc` and `@doc-latex` will
+  build the HTML and LaTeX documentation repsectively. (#5695, fixes #3760,
+  @Alizter)
+
 3.2.0 (17-05-2022)
 ------------------
 
diff --git a/src/dune_engine/action_builder.ml b/src/dune_engine/action_builder.ml
index 517695cd913..86896fb0744 100644
--- a/src/dune_engine/action_builder.ml
+++ b/src/dune_engine/action_builder.ml
@@ -151,6 +151,15 @@ module With_targets = struct
           (Targets.Files.create (Path.Build.Set.of_list file_targets))
     }
 
+  let add_directories t ~directory_targets =
+    { build = t.build
+    ; targets =
+        Targets.combine t.targets
+          (Targets.create
+             ~dirs:(Path.Build.Set.of_list directory_targets)
+             ~files:Path.Build.Set.empty)
+    }
+
   let map { build; targets } ~f = { build = map build ~f; targets }
 
   let map2 x y ~f =
diff --git a/src/dune_engine/action_builder.mli b/src/dune_engine/action_builder.mli
index 224154d9877..9dab2af0d9f 100644
--- a/src/dune_engine/action_builder.mli
+++ b/src/dune_engine/action_builder.mli
@@ -18,6 +18,8 @@ module With_targets : sig
 
   val add : 'a t -> file_targets:Path.Build.t list -> 'a t
 
+  val add_directories : 'a t -> directory_targets:Path.Build.t list -> 'a t
+
   val map : 'a t -> f:('a -> 'b) -> 'b t
 
   val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t
diff --git a/src/dune_rules/command.ml b/src/dune_rules/command.ml
index 124fb220403..3195af4a5cd 100644
--- a/src/dune_rules/command.ml
+++ b/src/dune_rules/command.ml
@@ -97,7 +97,7 @@ let dep_prog = function
   | Ok p -> Action_builder.path p
   | Error _ -> Action_builder.return ()
 
-let run ~dir ?stdout_to prog args =
+let run ~dir ?sandbox ?stdout_to prog args =
   Action_builder.With_targets.add ~file_targets:(Option.to_list stdout_to)
     (let open Action_builder.With_targets.O in
     let+ () = Action_builder.with_no_targets (dep_prog prog)
@@ -108,7 +108,7 @@ let run ~dir ?stdout_to prog args =
       | None -> action
       | Some path -> Action.with_stdout_to path action
     in
-    Action.Full.make (Action.chdir dir action))
+    Action.Full.make ?sandbox (Action.chdir dir action))
 
 let run' ~dir prog args =
   let open Action_builder.O in
diff --git a/src/dune_rules/command.mli b/src/dune_rules/command.mli
index 44b08124edb..1141d97f9ab 100644
--- a/src/dune_rules/command.mli
+++ b/src/dune_rules/command.mli
@@ -79,6 +79,7 @@ end
    we can use the constructor [S] to concatenate lists instead. *)
 val run :
      dir:Path.t
+  -> ?sandbox:Sandbox_config.t
   -> ?stdout_to:Path.Build.t
   -> Action.Prog.t
   -> Args.any Args.t list
diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml
index b96273d2d7d..4bbe0060a12 100644
--- a/src/dune_rules/coq_module.ml
+++ b/src/dune_rules/coq_module.ml
@@ -70,6 +70,10 @@ type obj_files_mode =
   | Build
   | Install
 
+let glob_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".glob")
+
 (* XXX: Remove the install .coq-native hack once rules can output targets in
    multiple subdirs *)
 let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
diff --git a/src/dune_rules/coq_module.mli b/src/dune_rules/coq_module.mli
index d96fc3fbbcd..1dd1395701c 100644
--- a/src/dune_rules/coq_module.mli
+++ b/src/dune_rules/coq_module.mli
@@ -40,6 +40,8 @@ val name : t -> Name.t
 
 val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val glob_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
 (** Some of the object files should not be installed, we control this with the
     following parameter *)
 type obj_files_mode =
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 4a180cf6bbe..635d10d6a5e 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -106,6 +106,7 @@ module Context = struct
   type 'a t =
     { coqdep : Action.Prog.t
     ; coqc : Action.Prog.t * Path.Build.t
+    ; coqdoc : Action.Prog.t
     ; wrapper_name : string
     ; dir : Path.Build.t
     ; expander : Expander.t
@@ -190,6 +191,16 @@ module Context = struct
       in
       Resolve.args args
 
+  let coqdoc_file_flags cctx =
+    let file_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 ]
+
   (* compute include flags and mlpack rules *)
   let setup_ml_deps ~lib_db libs theories =
     (* Pair of include flags and paths to mlpack *)
@@ -250,9 +261,11 @@ module Context = struct
       setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs
     and+ coqdep = rr "coqdep"
     and+ coqc = rr "coqc"
+    and+ coqdoc = rr "coqdoc"
     and+ profile_flags = Super_context.coq sctx ~dir in
     { coqdep
     ; coqc = (coqc, coqc_dir)
+    ; coqdoc
     ; wrapper_name
     ; dir
     ; expander
@@ -372,6 +385,79 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   Context.coqc cctx (Command.Args.dyn coq_flags :: file_flags)
   >>| Action.Full.add_sandbox sandbox
 
+module Coqdoc_mode = struct
+  type t =
+    | Html
+    | Latex
+
+  let flag = function
+    | Html -> "--html"
+    | Latex -> "--latex"
+
+  let directory t obj_dir (theory : Coq_lib_name.t) =
+    Path.Build.relative obj_dir
+      (Coq_lib_name.to_string theory
+      ^
+      match t with
+      | Html -> ".html"
+      | Latex -> ".tex")
+
+  let alias t ~dir =
+    match t with
+    | Html -> Alias.doc ~dir
+    | Latex -> Alias.make (Alias.Name.of_string "doc-latex") ~dir
+end
+
+let coqdoc_directory_targets ~dir:obj_dir (theory : Coq_stanza.Theory.t) =
+  let loc, 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
+    ~theories_deps coq_modules =
+  let obj_dir = cctx.dir in
+  let doc_dir = Coqdoc_mode.directory mode obj_dir name in
+  let file_flags =
+    let globs =
+      let open Action_builder.O in
+      let* theories_deps = Resolve.read theories_deps in
+      Action_builder.of_memo
+      @@
+      let open Memo.O in
+      let+ deps =
+        Memo.parallel_map theories_deps ~f:(fun theory ->
+            let+ theory_dirs = Context.directories_of_lib ~sctx theory in
+            Dep.Set.of_list_map theory_dirs ~f:(fun dir ->
+                (* TODO *)
+                Glob.of_string_exn Loc.none "*.{glob}"
+                |> Glob.to_pred
+                |> File_selector.create ~dir:(Path.build dir)
+                |> Dep.file_selector))
+      in
+      Command.Args.Hidden_deps (Dep.Set.union_all deps)
+    in
+    [ Command.Args.S file_flags
+    ; A "--toc"
+    ; A Coqdoc_mode.(flag mode)
+    ; A "-d"
+    ; Path (Path.build doc_dir)
+    ; Deps (List.map ~f:Path.build @@ List.map ~f:Coq_module.source coq_modules)
+    ; Dyn globs
+    ; Hidden_deps
+        (Dep.Set.of_files @@ List.map ~f:Path.build
+        @@ List.map ~f:(Coq_module.glob_file ~obj_dir) coq_modules)
+    ]
+  in
+  Command.run ~sandbox:Sandbox_config.needs_sandboxing
+    ~dir:(Path.build cctx.dir) cctx.coqdoc file_flags
+  |> Action_builder.With_targets.map
+       ~f:
+         (Action.Full.map ~f:(fun coqdoc ->
+              Action.Progn [ Action.mkdir (Path.build doc_dir); coqdoc ]))
+  |> Action_builder.With_targets.add_directories ~directory_targets:[ doc_dir ]
+
 module Module_rule = struct
   type t =
     { coqdep : Action.Full.t Action_builder.With_targets.t
@@ -425,8 +511,9 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     let theories_deps =
       Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result
     in
-    let theory_dirs = Coq_sources.directories coq_dir_contents ~name in
-    let theory_dirs = Path.Build.Set.of_list theory_dirs in
+    let theory_dirs =
+      Coq_sources.directories coq_dir_contents ~name |> Path.Build.Set.of_list
+    in
     let coqc_dir = (Super_context.context sctx).build_dir in
     Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~theory_dirs
       s.buildable
@@ -441,11 +528,28 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     in
     source_rule ~sctx theories
   in
+  let loc = s.buildable.loc in
+  let* () =
+    let rule =
+      let file_flags = Context.coqdoc_file_flags cctx in
+      fun mode ->
+        let* () =
+          coqdoc_rule cctx ~sctx ~mode ~theories_deps:cctx.theories_deps
+            ~name:s.name ~file_flags coq_modules
+          |> Super_context.add_rule ~loc ~dir sctx
+        in
+        Coqdoc_mode.directory mode cctx.dir name
+        |> Path.build |> Action_builder.path
+        |> Rules.Produce.Alias.add_deps (Coqdoc_mode.alias mode ~dir) ~loc
+    in
+    let* () = rule Html in
+    rule Latex
+  in
   List.concat_map coq_modules ~f:(fun m ->
       let cctx = Context.for_module cctx m in
       let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in
       [ coqc; coqdep ])
-  |> Super_context.add_rules ~loc:s.buildable.loc ~dir sctx
+  |> 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
diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli
index 7ff71d0b809..dedd3108e90 100644
--- a/src/dune_rules/coq_rules.mli
+++ b/src/dune_rules/coq_rules.mli
@@ -17,6 +17,9 @@ module Bootstrap : sig
     | Bootstrap_prelude  (** We are compiling the prelude itself *)
 end
 
+val coqdoc_directory_targets :
+  dir:Path.Build.t -> Coq_stanza.Theory.t -> Loc.t Path.Build.Map.t
+
 val setup_rules :
      sctx:Super_context.t
   -> dir:Path.Build.t
diff --git a/src/dune_rules/gen_rules.ml b/src/dune_rules/gen_rules.ml
index 2b8353863e0..e70fe462cb4 100644
--- a/src/dune_rules/gen_rules.ml
+++ b/src/dune_rules/gen_rules.ml
@@ -277,6 +277,24 @@ let gen_rules sctx dir_contents cctxs expander
   let+ () = define_all_alias ~dir:ctx_dir ~scope ~js_targets in
   cctxs
 
+let collect_directory_targets sctx ~init ~dir =
+  match Super_context.stanzas_in sctx ~dir with
+  | None -> init
+  | Some { Dir_with_dune.data = stanzas; ctx_dir = dir; _ } ->
+    List.fold_left stanzas ~init ~f:(fun acc stanza ->
+        match stanza with
+        | Coq_stanza.Theory.T m ->
+          Coq_rules.coqdoc_directory_targets ~dir m
+          |> Path.Build.Map.union acc ~f:(fun path loc1 loc2 ->
+                 User_error.raise
+                   [ Pp.textf
+                       "the following both define the directory target: %s"
+                       (Path.Build.to_string path)
+                   ; Pp.textf "- %s" (Loc.to_file_colon_line loc1)
+                   ; Pp.textf "- %s" (Loc.to_file_colon_line loc2)
+                   ])
+        | _ -> acc)
+
 let gen_rules sctx dir_contents cctxs ~source_dir ~dir :
     (Loc.t * Compilation_context.t) list Memo.t =
   let* expander =
@@ -429,7 +447,8 @@ let gen_rules ~sctx ~dir components : Build_config.gen_rules_result Memo.t =
         Memo.return
           (Build_config.Rules
              { build_dir_only_sub_dirs = S.These subdirs
-             ; directory_targets
+             ; directory_targets =
+                 collect_directory_targets sctx ~dir ~init:directory_targets
              ; rules
              })))
 
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/base.v b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/base.v
new file mode 100644
index 00000000000..63af1913bd9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/base.v
@@ -0,0 +1,5 @@
+
+Variant Or (A B : Set) : Set :=
+| inl : A -> Or A B
+| inr : B -> Or A B
+.
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune
new file mode 100644
index 00000000000..e8c213a957c
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune
@@ -0,0 +1,21 @@
+(rule
+ (targets
+  (dir base.html))
+ (action
+  (progn
+   (run mkdir base.html)
+   (run touch base.html/base.base.html))))
+
+(rule
+ (targets
+  (dir base.tex))
+ (action
+  (progn
+   (run mkdir base.tex)
+   (run touch base.tex/base.base.tex))))
+
+(coq.theory
+ (name base)
+ (package base)
+ (modules base)
+ (synopsis "Base Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune-project
new file mode 100644
index 00000000000..a1049fe7f56
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/dune-project
@@ -0,0 +1,6 @@
+(lang dune 3.1)
+(using directory-targets 0.1)
+(using coq 0.3)
+
+(package
+ (name base))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t
new file mode 100644
index 00000000000..33464d0c71f
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-dir-target-clash.t/run.t
@@ -0,0 +1,8 @@
+We try to build the documentation but there will be a clash between the
+directory targets. Notice how the tex one fails before html one.
+  $ dune build @check
+  Error: the following both define the directory target:
+  _build/default/base.tex
+  - dune:9
+  - dune:18
+  [1]
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AA/aa.v b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AA/aa.v
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AB/ab.v b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AB/ab.v
new file mode 100644
index 00000000000..497f743f440
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/AB/ab.v
@@ -0,0 +1 @@
+Require Import AA.aa.
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/dune b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/dune
new file mode 100644
index 00000000000..66eb821cc35
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/A/dune
@@ -0,0 +1,3 @@
+(include_subdirs qualified)
+(coq.theory
+ (name A))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/b.v b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/b.v
new file mode 100644
index 00000000000..dbbe84300ce
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/b.v
@@ -0,0 +1 @@
+From A Require Import AB.ab.
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/dune b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/dune
new file mode 100644
index 00000000000..974c95dbf71
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/B/dune
@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name B)
+ (theories A))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/dune-project
new file mode 100644
index 00000000000..227be0346ac
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.0)
+(using coq 0.3)
+(name CoqTest)
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t
new file mode 100644
index 00000000000..32e083c7338
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc-multi-theory.t/run.t
@@ -0,0 +1,60 @@
+HTML
+----
+
+First we build the doc alias for the first theory
+  $ dune build @A/doc
+The first theory doc is built
+  $ ls _build/default/A/A.html
+  A.AA.aa.html
+  A.AB.ab.html
+  coqdoc.css
+  index.html
+  toc.html
+Check that the second is not built
+  $ ls _build/default/
+  A
+Clean
+  $ dune clean
+
+Next we build the doc for the second theory
+  $ dune build @B/doc
+Check that the first theory doc is not built
+  $ ls _build/default/A/
+  AA
+  AB
+Check that the second theory doc is built
+  $ ls _build/default/B/B.html
+  B.b.html
+  coqdoc.css
+  index.html
+  toc.html
+Clean
+  $ dune clean
+
+
+LaTeX
+-----
+
+Next we test the LaTeX targets in the same manner
+  $ dune build @A/doc-latex
+The first theory doc is built
+  $ ls _build/default/A/A.tex
+  A.AA.aa.tex
+  A.AB.ab.tex
+  coqdoc.sty
+Check that the second is not built
+  $ ls _build/default
+  A
+Clean
+  $ dune clean
+
+Next we build the doc for the second theory
+  $ dune build @B/doc-latex
+Check that the first theory doc is not built
+  $ ls _build/default/A
+  AA
+  AB
+Check that the second theory doc is built
+  $ ls _build/default/B/B.tex
+  B.b.tex
+  coqdoc.sty
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/bar.v b/test/blackbox-tests/test-cases/coq/coqdoc.t/bar.v
new file mode 100644
index 00000000000..4627b76131c
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/bar.v
@@ -0,0 +1,3 @@
+From basic Require Import foo.
+
+Definition mynum (i : mynat) := 3.
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/dune b/test/blackbox-tests/test-cases/coq/coqdoc.t/dune
new file mode 100644
index 00000000000..6c57505fa27
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name basic)
+ (package base)
+ (modules :standard)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdoc.t/dune-project
new file mode 100644
index 00000000000..a1049fe7f56
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/dune-project
@@ -0,0 +1,6 @@
+(lang dune 3.1)
+(using directory-targets 0.1)
+(using coq 0.3)
+
+(package
+ (name base))
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/foo.v b/test/blackbox-tests/test-cases/coq/coqdoc.t/foo.v
new file mode 100644
index 00000000000..53e0ce1b152
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t
new file mode 100644
index 00000000000..e2174daafaf
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/coqdoc.t/run.t
@@ -0,0 +1,41 @@
+We build the coqdoc html target:
+  $ dune build basic.html/
+
+Now we inspect it:
+  $ ls _build/default/basic.html
+  basic.bar.html
+  basic.foo.html
+  coqdoc.css
+  index.html
+  toc.html
+
+We buuild the coqdoc latex target:
+  $ dune build basic.tex/
+
+Now we inspect it:
+  $ ls _build/default/basic.tex
+  basic.bar.tex
+  basic.foo.tex
+  coqdoc.sty
+
+Next from a clean build we make sure that @all does *not* build any doc targets:
+  $ dune clean
+  $ dune build @all
+Note that this currently works due to a bug in @all detecting directory targets.
+  $ ls _build/default
+  META.base
+  bar.glob
+  bar.v
+  bar.v.d
+  bar.vo
+  bar.vok
+  bar.vos
+  base.dune-package
+  base.install
+  foo.glob
+  foo.v
+  foo.v.d
+  foo.vo
+  foo.vok
+  foo.vos
+