diff --git a/CHANGES.md b/CHANGES.md
index 0c1e36e6748..e3af170f3c6 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -91,6 +91,8 @@ Unreleased
 
 - [coq] Add `-q` flag to `:standard` `coqc` flags , fixes #3924, (#3931 , @ejgallego)
 
+- Add support for Coq's native compute compilation mode (@ejgallego, #3210)
+
 2.7.1 (2/09/2020)
 -----------------
 
diff --git a/Makefile b/Makefile
index b130a996c47..ad47ac51a68 100644
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,7 @@ BIN := ./dune.exe
 TEST_DEPS := \
 bisect_ppx \
 cinaps \
-coq \
+"coq>=8.12.1" \
 core_bench \
 "csexp>=1.3.0" \
 js_of_ocaml \
diff --git a/doc/dune-files.rst b/doc/dune-files.rst
index d0d113bf3d2..6b5c599ad5a 100644
--- a/doc/dune-files.rst
+++ b/doc/dune-files.rst
@@ -1625,6 +1625,7 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
      (modules <ordered_set_lang>)
      (libraries <ocaml_libraries>)
      (flags <coq_flags>)
+     (mode <coq_native_mode>)
      (theories <coq_theories>))
 
 The stanza will build all ``.v`` files on the given directory. The semantics of fields is:
@@ -1668,6 +1669,17 @@ The stanza will build all ``.v`` files on the given directory. The semantics of
   composition with the Coq's standard library is supported, but in
   this case the ``Coq`` prefix will be made available in a qualified
   way. Since Coq's lang version ``0.2``.
+- you can enable the production of Coq's native compiler object files
+  by setting ``<coq_native_mode>`` to ``native``, this will pass
+  ``-native-compiler on`` to Coq and install the corresponding object
+  files under `.coq-native`. Note that the support for native compute
+  is **experimental**, and requires Coq >= 8.12.1; moreover, depending
+  libraries *must* be built with ``(mode native)`` too for this to
+  work; also Coq must be configured to support native
+  compilation. Note that Dune will by explicitly disable output of
+  native compilation objects when `(mode vo)` even if the default
+  Coq's configure flag enabled it. This will be improved in the
+  future.
 
 Recursive qualification of modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1899,9 +1911,9 @@ a typical ``dune-workspace`` file looks like:
 .. code:: scheme
 
     (lang dune 2.8)
-    (context (opam (switch 4.02.3)))
-    (context (opam (switch 4.03.0)))
-    (context (opam (switch 4.04.0)))
+    (context (opam (switch 4.07.1)))
+    (context (opam (switch 4.08.1)))
+    (context (opam (switch 4.11.1)))
 
 The rest of this section describe the stanzas available.
 
diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
index af986905087..ff447aac629 100644
--- a/src/dune_rules/coq_lib.ml
+++ b/src/dune_rules/coq_lib.ml
@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 open! Stdune
diff --git a/src/dune_rules/coq_lib_name.mli b/src/dune_rules/coq_lib_name.mli
index 03cbd1950eb..a4978bc7aa2 100644
--- a/src/dune_rules/coq_lib_name.mli
+++ b/src/dune_rules/coq_lib_name.mli
@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 open! Stdune
diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/coq_mode.ml
new file mode 100644
index 00000000000..1bf1d2d6f52
--- /dev/null
+++ b/src/dune_rules/coq_mode.ml
@@ -0,0 +1,10 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+type t =
+  | VoOnly
+  | Native
+
+let decode = Dune_lang.Decoder.(enum [ ("vo", VoOnly); ("native", Native) ])
diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli
new file mode 100644
index 00000000000..ebdea59ee2d
--- /dev/null
+++ b/src/dune_rules/coq_mode.mli
@@ -0,0 +1,10 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+type t =
+  | VoOnly
+  | Native
+
+val decode : t Dune_lang.Decoder.t
diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml
index 6a68e7ee717..e93da5bfbc3 100644
--- a/src/dune_rules/coq_module.ml
+++ b/src/dune_rules/coq_module.ml
@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 open! Stdune
@@ -39,23 +40,44 @@ let name x = x.name
 let build_vo_dir ~obj_dir x =
   List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative
 
-type obj =
-  | Dep
-  | Aux
-  | Glob
-  | Obj
-
-let fname_of_obj t obj =
-  match obj with
-  | Dep -> t.name ^ ".v.d"
-  | Aux -> "." ^ t.name ^ ".aux"
-  | Glob -> t.name ^ ".glob"
-  | Obj -> t.name ^ ".vo"
-
-let obj_file t obj ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir t in
-  let fname = fname_of_obj t obj in
-  Path.Build.relative vo_dir fname
+let cmxs_of_mod ~wrapper_name x =
+  let native_base =
+    "N" ^ String.concat ~sep:"_" ((wrapper_name :: x.prefix) @ [ x.name ])
+  in
+  [ native_base ^ ".cmi"; native_base ^ ".cmxs" ]
+
+let dep_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir (x.name ^ ".v.d")
+
+type obj_files_mode =
+  | Build
+  | Install
+
+(* 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 =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  let install_vo_dir = String.concat ~sep:"/" x.prefix in
+  let native_objs =
+    match mode with
+    | Coq_mode.Native ->
+      let cmxs_obj = cmxs_of_mod ~wrapper_name x in
+      List.map
+        ~f:(fun x ->
+          ( Path.Build.relative vo_dir x
+          , Filename.(concat (concat install_vo_dir ".coq-native") x) ))
+        cmxs_obj
+    | VoOnly -> []
+  in
+  let obj_files =
+    match obj_files_mode with
+    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
+    | Install -> [ x.name ^ ".vo" ]
+  in
+  List.map obj_files ~f:(fun fname ->
+      (Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname))
+  @ native_objs
 
 let to_dyn { source; prefix; name } =
   let open Dyn.Encoder in
diff --git a/src/dune_rules/coq_module.mli b/src/dune_rules/coq_module.mli
index 1dcb648cbad..5c48f061c71 100644
--- a/src/dune_rules/coq_module.mli
+++ b/src/dune_rules/coq_module.mli
@@ -38,13 +38,23 @@ val prefix : t -> string list
 
 val name : t -> Name.t
 
-type obj =
-  | Dep
-  | Aux
-  | Glob
-  | Obj
-
-val obj_file : t -> obj -> obj_dir:Path.Build.t -> Path.Build.t
+val dep_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 =
+  | Build
+  | Install
+
+(** This returns a list of pairs [(obj_file, install_path)] due to native files
+    having a different install location *)
+val obj_files :
+     t
+  -> wrapper_name:string
+  -> mode:Coq_mode.t
+  -> obj_dir:Path.Build.t
+  -> obj_files_mode:obj_files_mode
+  -> (Path.Build.t * string) list
 
 val to_dyn : t -> Dyn.t
 
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 1e0099df6c1..f13b0bbb56e 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -4,6 +4,7 @@ open! Dune_engine
 (* (c) MINES ParisTech 2018-2019               *)
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
+(* Written by: Rudi Grinberg *)
 
 open! Stdune
 open Coq_stanza
@@ -19,6 +20,13 @@ module Util = struct
         let info = Lib.info t in
         Lib_info.src_dir info)
 
+  let coq_nativelib_cmi_dirs ts =
+    List.fold_left ts ~init:Path.Set.empty ~f:(fun acc t ->
+        let info = Lib.info t in
+        (* We want the cmi files *)
+        let obj_dir = Obj_dir.public_cmi_dir (Lib_info.obj_dir info) in
+        Path.Set.add acc obj_dir)
+
   let include_flags ts = include_paths ts |> Lib.L.to_iflags
 
   (* coqdep expects an mlpack file next to the sources otherwise it
@@ -80,6 +88,13 @@ end
 (* get_libraries from Coq's ML dependencies *)
 let libs_of_coq_deps ~lib_db = Result.List.map ~f:(Lib.DB.resolve lib_db)
 
+let select_native_mode ~sctx ~(buildable : Buildable.t) =
+  let profile = (SC.context sctx).profile in
+  if Profile.is_dev profile then
+    Coq_mode.VoOnly
+  else
+    snd buildable.mode
+
 module Context = struct
   type 'a t =
     { coqdep : Action.Prog.t
@@ -95,6 +110,9 @@ module Context = struct
     ; boot_type : Bootstrap.t
     ; build_dir : Path.Build.t
     ; profile_flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Coq_mode.t
+    ; native_includes : Path.Set.t Or_exn.t
+    ; native_theory_includes : Path.Build.Set.t Or_exn.t
     }
 
   let coqc ?stdout_to t args =
@@ -137,6 +155,34 @@ module Context = struct
     in
     [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ]
 
+  let coqc_native_flags cctx : _ Command.Args.t =
+    match cctx.mode with
+    | Coq_mode.VoOnly ->
+      Command.Args.As
+        [ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ]
+    | Coq_mode.Native ->
+      let args =
+        let open Result.O in
+        let* native_includes = cctx.native_includes in
+        let include_ dir acc = Command.Args.Path dir :: A "-nI" :: acc in
+        let native_include_ml_args =
+          Path.Set.fold native_includes ~init:[] ~f:include_
+        in
+        let+ native_theory_includes = cctx.native_theory_includes in
+        let native_include_theory_output =
+          Path.Build.Set.fold native_theory_includes ~init:[] ~f:(fun dir acc ->
+              include_ (Path.build dir) acc)
+        in
+        (* This dir is relative to the file, by default [.coq-native/] *)
+        Command.Args.S
+          [ Command.Args.As [ "-native-output-dir"; "." ]
+          ; Command.Args.As [ "-native-compiler"; "on" ]
+          ; Command.Args.S (List.rev native_include_ml_args)
+          ; Command.Args.S (List.rev native_include_theory_output)
+          ]
+      in
+      Command.of_result args
+
   (* compute include flags and mlpack rules *)
   let setup_ml_deps ~lib_db libs theories =
     (* Pair of include flags and paths to mlpack *)
@@ -152,7 +198,24 @@ module Context = struct
           (* If the mlpack files don't exist, don't fail *)
           Build.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)) )
 
-  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps
+  let directories_of_lib ~sctx lib =
+    let name = Coq_lib.name lib in
+    let dir = Coq_lib.src_root lib in
+    let dir_contents = Dir_contents.get sctx ~dir in
+    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 Or_exn.t) ~theory_dirs =
+    match mode with
+    | Coq_mode.Native ->
+      Result.map theories_deps ~f:(fun theories_deps ->
+          List.fold_left theories_deps ~init:theory_dirs ~f:(fun acc lib ->
+              let theory_dirs = directories_of_lib ~sctx lib in
+              Path.Build.Set.(union acc (of_list theory_dirs))))
+    | Coq_mode.VoOnly -> Or_exn.return Path.Build.Set.empty
+
+  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~theory_dirs
       (buildable : Buildable.t) =
     let loc = buildable.loc in
     let rr = resolve_program sctx ~dir ~loc in
@@ -163,6 +226,14 @@ module Context = struct
     let ml_flags, mlpack_rule =
       setup_ml_deps ~lib_db buildable.libraries theories_deps
     in
+    let mode = select_native_mode ~sctx ~buildable in
+    let native_includes =
+      Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel")
+      |> Result.map ~f:(fun lib -> Util.coq_nativelib_cmi_dirs [ lib ])
+    in
+    let native_theory_includes =
+      setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs
+    in
     let build_dir = (Super_context.context sctx).build_dir in
     { coqdep = rr "coqdep"
     ; coqc = (rr "coqc", coqc_dir)
@@ -177,6 +248,9 @@ module Context = struct
     ; boot_type = Bootstrap.No_boot
     ; build_dir
     ; profile_flags = Super_context.coq sctx ~dir
+    ; mode
+    ; native_includes
+    ; native_theory_includes
     }
 
   let for_module t coq_module =
@@ -240,7 +314,7 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module
       :: deps )
 
 let deps_of ~dir ~boot_type coq_module =
-  let stdout_to = Coq_module.obj_file ~obj_dir:dir coq_module Dep in
+  let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
   Build.dyn_paths_unit
     (Build.map
        (Build.lines_of (Path.build stdout_to))
@@ -255,7 +329,7 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
     ; Dep (Path.build source)
     ]
   in
-  let stdout_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Dep in
+  let stdout_to = Coq_module.dep_file ~obj_dir:cctx.dir coq_module in
   (* Coqdep has to be called in the stanza's directory *)
   let open Build.With_targets.O in
   Build.with_no_targets cctx.mlpack_rule
@@ -265,10 +339,15 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
 let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
-    let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Obj in
-    let aux = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Aux in
-    let glob = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Glob in
-    [ Command.Args.Hidden_targets [ object_to; aux; glob ]
+    let wrapper_name, mode = (cctx.wrapper_name, cctx.mode) in
+    let objects_to =
+      Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:cctx.dir
+        ~obj_files_mode:Coq_module.Build coq_module
+      |> List.map ~f:fst
+    in
+    let native_flags = Context.coqc_native_flags cctx in
+    [ Command.Args.Hidden_targets objects_to
+    ; native_flags
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
     ]
@@ -329,19 +408,20 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
   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 coq_dir_contents = Dir_contents.coq dir_contents in
+
   let cctx =
     let wrapper_name = Coq_lib.wrapper theory in
-    (* Coq flags for depending libraries *)
     let theories_deps = Coq_lib.DB.requires coq_lib_db theory in
+    let theory_dirs = Coq_sources.directories coq_dir_contents ~name in
+    let theory_dirs = Path.Build.Set.of_list theory_dirs in
     let coqc_dir = (Super_context.context sctx).build_dir in
-    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps s.buildable
+    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~theory_dirs
+      s.buildable
   in
 
   (* List of modules to compile for this library *)
-  let coq_modules =
-    let coq = Dir_contents.coq dir_contents in
-    Coq_sources.library coq ~name
-  in
+  let coq_modules = Coq_sources.library coq_dir_contents ~name in
 
   let source_rule =
     let theories =
@@ -393,7 +473,8 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) =
 let install_rules ~sctx ~dir s =
   match s with
   | { Theory.package = None; _ } -> []
-  | { Theory.package = Some package; _ } ->
+  | { Theory.package = Some package; buildable; _ } ->
+    let mode = select_native_mode ~sctx ~buildable in
     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
@@ -417,21 +498,28 @@ let install_rules ~sctx ~dir s =
       else
         coq_plugins_install_rules ~scope ~package ~dst_dir s
     in
+    let wrapper_name = dst_suffix in
+    let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in
+    let to_dst f = Path.Local.to_string @@ Path.Local.relative dst_dir f in
+    let make_entry (orig_file : Path.Build.t) (dst_file : string) =
+      ( Some loc
+      , (* Entry.make Section.Lib_root ~dst:(to_dst (to_path dst_file))
+           orig_file) *)
+        Install.Entry.make Section.Lib_root ~dst:(to_dst dst_file) orig_file )
+    in
     Dir_contents.coq dir_contents
     |> Coq_sources.library ~name
     |> List.concat_map ~f:(fun (vfile : Coq_module.t) ->
-           let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in
-           let to_dst f =
-             Path.Local.to_string @@ Path.Local.relative dst_dir f
+           let obj_files =
+             Coq_module.obj_files ~wrapper_name ~mode ~obj_dir:dir
+               ~obj_files_mode:Coq_module.Install vfile
+             |> List.map
+                  ~f:(fun ((vo_file : Path.Build.t), (install_vo_file : string))
+                     -> make_entry vo_file install_vo_file)
            in
-           let vofile = Coq_module.obj_file ~obj_dir:dir vfile Obj in
            let vfile = Coq_module.source vfile in
-           let make_entry file =
-             ( Some loc
-             , Install.(Entry.make Lib_root ~dst:(to_dst (to_path file)) file)
-             )
-           in
-           [ make_entry vfile; make_entry vofile ])
+           let vfile_dst = to_path vfile in
+           make_entry vfile vfile_dst :: obj_files)
     |> List.rev_append coq_plugins_install_rules
 
 let coqpp_rules ~sctx ~dir (s : Coqpp.t) =
@@ -453,8 +541,9 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
       let coq_lib_db = Scope.coq_libs scope in
       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
-      s.buildable
+      ~theory_dirs s.buildable
   in
   let coq_module =
     let coq = Dir_contents.coq dir_contents in
diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli
index c3070625476..1ecaff74a94 100644
--- a/src/dune_rules/coq_rules.mli
+++ b/src/dune_rules/coq_rules.mli
@@ -2,6 +2,7 @@ open! Dune_engine
 
 (* This file is licensed under The MIT License *)
 (* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
 (* Build rules for Coq's .v -> .vo files *)
diff --git a/src/dune_rules/coq_sources.ml b/src/dune_rules/coq_sources.ml
index 562b74a9cb8..935fa7168ff 100644
--- a/src/dune_rules/coq_sources.ml
+++ b/src/dune_rules/coq_sources.ml
@@ -8,10 +8,17 @@ open Coq_stanza
    In Coq all libs are "wrapped" so including a module twice is not so bad. *)
 type t =
   { libraries : Coq_module.t list Coq_lib_name.Map.t
+  ; directories : Path.Build.t list Coq_lib_name.Map.t
+        (* [directories] is used to compute the include paths for Coq's native
+           mode *)
   ; extract : Coq_module.t Loc.Map.t
   }
 
-let empty = { libraries = Coq_lib_name.Map.empty; extract = Loc.Map.empty }
+let empty =
+  { libraries = Coq_lib_name.Map.empty
+  ; directories = Coq_lib_name.Map.empty
+  ; extract = Loc.Map.empty
+  }
 
 let coq_modules_of_files ~dirs =
   let filter_v_files (dir, local, files) =
@@ -31,10 +38,15 @@ let coq_modules_of_files ~dirs =
 
 let library t ~name = Coq_lib_name.Map.find_exn t.libraries name
 
+let directories t ~name = Coq_lib_name.Map.find_exn t.directories name
+
 let check_no_unqualified (loc, (qualif_mode : Dune_file.Include_subdirs.t)) =
   if qualif_mode = Include Unqualified then
     User_error.raise ~loc
-      [ Pp.text "(include_subdirs unqualified) is not supported yet" ]
+      [ Pp.text
+          "(include_subdirs unqualified) is not supported yet with (coq.theory \
+           ...) stanzas"
+      ]
 
 let extract t (stanza : Extraction.t) =
   Loc.Map.find_exn t.extract stanza.buildable.loc
@@ -47,10 +59,14 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
       let modules =
         Coq_module.eval ~dir:d.ctx_dir coq.modules ~standard:modules
       in
+      let directories =
+        Coq_lib_name.Map.add_exn acc.directories (snd 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
-      { acc with libraries }
+      { acc with directories; libraries }
     | Coq_stanza.Extraction.T extract ->
       let loc, prelude = extract.prelude in
       let m =
diff --git a/src/dune_rules/coq_sources.mli b/src/dune_rules/coq_sources.mli
index 5ff5dcb9ff0..89f9ac5001e 100644
--- a/src/dune_rules/coq_sources.mli
+++ b/src/dune_rules/coq_sources.mli
@@ -10,6 +10,8 @@ val empty : t
 (** Coq modules of library [name] is the Coq library name. *)
 val library : t -> name:Coq_lib_name.t -> Coq_module.t list
 
+val directories : t -> name:Coq_lib_name.t -> Path.Build.t list
+
 val extract : t -> Coq_stanza.Extraction.t -> Coq_module.t
 
 val of_dir :
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index 1cdfc8893e2..d7e14575c85 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/src/dune_rules/coq_stanza.ml
@@ -21,11 +21,15 @@ end
 
 let coq_syntax =
   Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)"
-    [ ((0, 1), `Since (1, 9)); ((0, 2), `Since (2, 5)) ]
+    [ ((0, 1), `Since (1, 9))
+    ; ((0, 2), `Since (2, 5))
+    ; ((0, 3), `Since (2, 8))
+    ]
 
 module Buildable = struct
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Coq_mode.t
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t
@@ -34,6 +38,10 @@ module Buildable = struct
   let decode =
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
+    and+ mode =
+      located
+        (field "mode" ~default:Coq_mode.VoOnly
+           (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ libraries =
       field "libraries" (repeat (located Lib_name.decode)) ~default:[]
     and+ theories =
@@ -41,7 +49,7 @@ module Buildable = struct
         (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode)
         ~default:[]
     in
-    { flags; libraries; theories; loc }
+    { flags; mode; libraries; theories; loc }
 end
 
 module Extraction = struct
diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli
index dd14ce1b550..9435c256cd8 100644
--- a/src/dune_rules/coq_stanza.mli
+++ b/src/dune_rules/coq_stanza.mli
@@ -4,6 +4,7 @@ open Import
 module Buildable : sig
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Coq_mode.t
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t
diff --git a/src/dune_rules/profile.mli b/src/dune_rules/profile.mli
index 9fcbbcb26aa..977ec26cec6 100644
--- a/src/dune_rules/profile.mli
+++ b/src/dune_rules/profile.mli
@@ -1,5 +1,5 @@
 (** Defines build profile for dune. Only one profile is active per context. Some
-    profiles are treat specially by dune. *)
+    profiles are treated specially by dune. *)
 open! Import
 
 type t =
diff --git a/test/blackbox-tests/test-cases/coq/github3624.t/run.t b/test/blackbox-tests/test-cases/coq/github3624.t/run.t
index ecf8c83b1be..6dba3d9b862 100644
--- a/test/blackbox-tests/test-cases/coq/github3624.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/github3624.t/run.t
@@ -5,4 +5,4 @@ In github #3624, dune created a dune-project with an incorrect using line.
   >  (name foo))
   > EOF
   $ dune build 2>&1 | grep using
-  Info: Appending this line to dune-project: (using coq 0.2)
+  Info: Appending this line to dune-project: (using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v
new file mode 100644
index 00000000000..afe3c3b25d9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/bar.v
@@ -0,0 +1,3 @@
+From foo Require Import foo.
+
+Definition mynum (i : mynat) := 3.
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune
new file mode 100644
index 00000000000..632f5a43a55
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/bar/dune
@@ -0,0 +1,7 @@
+(coq.theory
+ (name bar)
+ (package base)
+ (mode native)
+ (theories foo)
+ (modules :standard)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/base.opam b/test/blackbox-tests/test-cases/coq/native-compose.t/base.opam
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/dune
new file mode 100644
index 00000000000..b53cf1eb053
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/dune
@@ -0,0 +1,3 @@
+(rule
+ (alias default)
+ (action (echo "%{read:base.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project b/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project
new file mode 100644
index 00000000000..23ca7faaa0e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.8)
+
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune
new file mode 100644
index 00000000000..72c8061029f
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name foo)
+ (package base)
+ (mode native)
+ (modules :standard)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v
new file mode 100644
index 00000000000..53e0ce1b152
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/foo/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
new file mode 100644
index 00000000000..c03453c21e9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
@@ -0,0 +1,22 @@
+  $ dune build --profile=release --display short --debug-dependency-path @all
+        coqdep bar/bar.v.d
+        coqdep foo/foo.v.d
+          coqc foo/.foo.aux,foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
+          coqc bar/.bar.aux,bar/Nbar_bar.{cmi,cmxs},bar/bar.{glob,vo}
+
+  $ dune build --profile=release --debug-dependency-path @default
+  lib: [
+    "_build/install/default/lib/base/META"
+    "_build/install/default/lib/base/dune-package"
+    "_build/install/default/lib/base/opam"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmi" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmi"}
+    "_build/install/default/lib/coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs" {"coq/user-contrib/bar/.coq-native/Nbar_bar.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/bar/bar.v" {"coq/user-contrib/bar/bar.v"}
+    "_build/install/default/lib/coq/user-contrib/bar/bar.vo" {"coq/user-contrib/bar/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi"}
+    "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/foo/foo.v" {"coq/user-contrib/foo/foo.v"}
+    "_build/install/default/lib/coq/user-contrib/foo/foo.vo" {"coq/user-contrib/foo/foo.vo"}
+  ]
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/bar.v b/test/blackbox-tests/test-cases/coq/native-single.t/bar.v
new file mode 100644
index 00000000000..4627b76131c
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-single.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/native-single.t/base.opam b/test/blackbox-tests/test-cases/coq/native-single.t/base.opam
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/dune b/test/blackbox-tests/test-cases/coq/native-single.t/dune
new file mode 100644
index 00000000000..11e0122c97d
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-single.t/dune
@@ -0,0 +1,10 @@
+(coq.theory
+ (name basic)
+ (package base)
+ (mode native)
+ (modules :standard)
+ (synopsis "Test Coq library"))
+
+(rule
+ (alias default)
+ (action (echo "%{read:base.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/dune-project b/test/blackbox-tests/test-cases/coq/native-single.t/dune-project
new file mode 100644
index 00000000000..23ca7faaa0e
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-single.t/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.8)
+
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/foo.v b/test/blackbox-tests/test-cases/coq/native-single.t/foo.v
new file mode 100644
index 00000000000..53e0ce1b152
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-single.t/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t
new file mode 100644
index 00000000000..1b01b367361
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t
@@ -0,0 +1,22 @@
+  $ dune build --profile=release --display short --debug-dependency-path @all
+        coqdep bar.v.d
+        coqdep foo.v.d
+          coqc .foo.aux,Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          coqc .bar.aux,Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
+
+  $ dune build --profile=release --debug-dependency-path @default
+  lib: [
+    "_build/install/default/lib/base/META"
+    "_build/install/default/lib/base/dune-package"
+    "_build/install/default/lib/base/opam"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"}
+    "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"}
+  ]