diff --git a/doc/coq.rst b/doc/coq.rst
index 9e8126fb125e..8e4784bba709 100644
--- a/doc/coq.rst
+++ b/doc/coq.rst
@@ -142,19 +142,10 @@ The semantics of the fields are:
   You may still use installed libraries in your Coq project, but there is
   currently no way for Dune to know about it.
 
-- You can enable the production of Coq's native compiler object files by setting
-  ``<coq_native_mode>`` to ``native``. This passes ``-native-compiler on`` to
-  Coq and install the corresponding object files under ``.coq-native``, when in
-  the ``release`` profile. The regular ``dev`` profile skips native compilation
-  to make the build faster. This has been available since :ref:`Coq lang
-  0.3<coq-lang>`.
-
-  Please note: support for ``native_compute`` is **experimental** and requires a
-  version of Coq later than 8.12.1. Furthermore, dependent theories *must* be
-  built with the ``(mode native)`` enabled. In addition to that, Coq must be
-  configured to support native compilation. Dune explicitly disables the
-  generation of native compilation objects when ``(mode vo)`` is enabled,
-  irrespective of the configuration of Coq. This will be improved in the future.
+- From version :ref:`Coq lang 0.6<coq-lang>` onwards, the native mode can be
+  automatically detected by Dune by querying ``coqc -config``. You may override
+  this by specifying ``<coq_native_mode>``. Before :ref:`Coq lang
+  0.6<coq-lang>`, the native mode must be manually specified.
 
 Coq Documentation
 ~~~~~~~~~~~~~~~~~
@@ -249,8 +240,11 @@ The supported Coq language versions (not the version of Coq) are:
 - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9
   for Coq >= 8.14).
 - ``0.4``: Support for interproject composition of theories.
-- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)`` field.
+- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)``
+  field.
 - ``0.6``: Support for ``(stdlib no)``.
+- ``0.7``: Support for automatic handling of native compilation according to Coq
+  compilation.
 
 .. _coq-lang-1.0:
 
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 870cc0566fd3..7d5f348a04b1 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -178,9 +178,19 @@ end
 (* get_libraries from Coq's ML dependencies *)
 let libs_of_coq_deps ~lib_db = Resolve.Memo.List.map ~f:(Lib.DB.resolve lib_db)
 
-let select_native_mode ~sctx ~(buildable : Buildable.t) : Coq_mode.t =
-  let profile = (Super_context.context sctx).profile in
-  if Profile.is_dev profile then VoOnly else snd buildable.mode
+let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
+  match snd buildable.mode with
+  | Some x -> Memo.return x
+  | None -> (
+    if buildable.coq_lang_version < (0, 3) then Memo.return Coq_mode.Legacy
+    else if buildable.coq_lang_version < (0, 7) then Memo.return Coq_mode.VoOnly
+    else
+      let* coqc = resolve_program sctx ~dir ~loc:buildable.loc "coqc" in
+      let+ config = Coq_config.make ~bin:(Action.Prog.ok_exn coqc) in
+      match Coq_config.by_name config "coq_native_compiler_default" with
+      | Some (Coq_config.Value.String "yes")
+      | Some (Coq_config.Value.String "ondemand") -> Coq_mode.Native
+      | _ -> Coq_mode.VoOnly)
 
 let rec resolve_first lib_db = function
   | [] -> assert false
@@ -330,7 +340,7 @@ module Context = struct
     let ml_flags, mlpack_rule =
       Coq_plugin.of_buildable ~context ~theories_deps ~lib_db buildable
     in
-    let mode = select_native_mode ~sctx ~buildable in
+    let* mode = select_native_mode ~sctx ~dir buildable in
     let* native_includes =
       let open Resolve.Memo.O in
       resolve_first lib_db [ "coq-core.kernel"; "coq.kernel" ] >>| fun lib ->
@@ -687,8 +697,8 @@ let install_rules ~sctx ~dir s =
   match s with
   | { Theory.package = None; _ } -> Memo.return []
   | { Theory.package = Some package; buildable; _ } ->
-    let mode = select_native_mode ~sctx ~buildable in
     let loc = s.buildable.loc in
+    let* mode = select_native_mode ~sctx ~dir buildable in
     let* scope = Scope.DB.find_by_dir dir in
     let* dir_contents = Dir_contents.get sctx ~dir in
     let name = snd s.name in
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index e01d61a715fc..216520e0813c 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/src/dune_rules/coq_stanza.ml
@@ -33,7 +33,7 @@ module Buildable = struct
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
-    ; mode : Loc.t * Coq_mode.t
+    ; mode : Loc.t * Coq_mode.t option
     ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
@@ -57,11 +57,8 @@ module Buildable = struct
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
     and+ mode =
-      let default =
-        if coq_lang_version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly
-      in
       located
-        (field "mode" ~default
+        (field_o "mode"
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ use_stdlib =
       field ~default:true "stdlib"
diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli
index 48084c7a7cc5..dff1138760bd 100644
--- a/src/dune_rules/coq_stanza.mli
+++ b/src/dune_rules/coq_stanza.mli
@@ -4,7 +4,7 @@ module Buildable : sig
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
-    ; mode : Loc.t * Coq_mode.t
+    ; mode : Loc.t * Coq_mode.t option
     ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml plugins *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)