diff --git a/CHANGES.md b/CHANGES.md
index 7710dd144cc0..34fa6b2f452d 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -30,6 +30,10 @@ Unreleased
 
 - Auto-detect `dune-project` files as `dune` files in Emacs (#4222, @shonfeder)
 
+- Restore compatibility with Coq < 8.10 for coq-lang < 0.3 , document
+  that `(using coq 0.3)` does require Coq 8.10 at least (#4224, fixes
+  #4142, @ejgallego)
+
 2.8.2 (21/01/2021)
 ------------------
 
diff --git a/doc/dune-files.rst b/doc/dune-files.rst
index f36894781b1d..e711fae893fe 100644
--- a/doc/dune-files.rst
+++ b/doc/dune-files.rst
@@ -1642,9 +1642,10 @@ language version is absent, dune will automatically add this line with the
 latest Coq version to the project file once a ``(coq.theory ...)`` stanza is used anywhere.
 
 The supported Coq language versions are:
+
 - ``0.1``: basic Coq theory support,
 - ``0.2``: support for the ``theories`` field, and composition of theories in the same scope,
-- ``0.3``: support for ``(mode native)``.
+- ``0.3``: support for ``(mode native)``, requires Coq >= 8.10.
 
 Guarantees with respect to stability are not provided yet,
 however, as implementation of features progresses, we hope to reach
diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/coq_mode.ml
index 1bf1d2d6f52c..aa1e39855ded 100644
--- a/src/dune_rules/coq_mode.ml
+++ b/src/dune_rules/coq_mode.ml
@@ -3,7 +3,11 @@
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
+(* Legacy is used to signal that we are in a mode prior to Coq syntax
+   0.3 , where mode was not supported, this allows us support older
+   Coq compiler versions with coq-lang < 0.3 *)
 type t =
+  | Legacy
   | VoOnly
   | Native
 
diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/coq_mode.mli
index ebdea59ee2d0..91832040cf14 100644
--- a/src/dune_rules/coq_mode.mli
+++ b/src/dune_rules/coq_mode.mli
@@ -3,7 +3,11 @@
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
+(* Legacy is used to signal that we are in a mode prior to Coq syntax
+   0.3 , where mode was not supported, this allows us support older
+   Coq compiler versions with coq-lang < 0.3 *)
 type t =
+  | Legacy
   | VoOnly
   | Native
 
diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml
index e93da5bfbc34..10b7e3d98187 100644
--- a/src/dune_rules/coq_module.ml
+++ b/src/dune_rules/coq_module.ml
@@ -68,7 +68,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
           ( Path.Build.relative vo_dir x
           , Filename.(concat (concat install_vo_dir ".coq-native") x) ))
         cmxs_obj
-    | VoOnly -> []
+    | VoOnly | Legacy -> []
   in
   let obj_files =
     match obj_files_mode with
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 057d12d333a3..809c4a45cc17 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -157,6 +157,7 @@ module Context = struct
 
   let coqc_native_flags cctx : _ Command.Args.t =
     match cctx.mode with
+    | Coq_mode.Legacy -> Command.Args.As []
     | Coq_mode.VoOnly ->
       Command.Args.As
         [ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ]
@@ -214,7 +215,7 @@ module Context = struct
           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
+    | Coq_mode.VoOnly | Coq_mode.Legacy -> Or_exn.return Path.Build.Set.empty
 
   let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~theory_dirs
       (buildable : Buildable.t) =
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index d7e14575c853..8332b3391d3e 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/src/dune_rules/coq_stanza.ml
@@ -39,8 +39,10 @@ module Buildable = struct
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
     and+ mode =
+      let* version = Dune_lang.Syntax.get_exn coq_syntax in
+      let default = if version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly in
       located
-        (field "mode" ~default:Coq_mode.VoOnly
+        (field "mode" ~default
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ libraries =
       field "libraries" (repeat (located Lib_name.decode)) ~default:[]