diff --git a/CHANGES.md b/CHANGES.md
index 9f135b6158d3..b59da2272864 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -11,6 +11,8 @@ unreleased
 
 - Fix glob dependencies on installed directories (#1965, @rgrinberg)
 
+- Experimental Coq support (1466, @ejgallego)
+
 1.8.2 (10/03/2019)
 ------------------
 
diff --git a/Makefile b/Makefile
index 1bafa1802a84..78acd78de07f 100644
--- a/Makefile
+++ b/Makefile
@@ -28,8 +28,11 @@ test:
 test-js:
 	$(BIN) build @runtest-js
 
+test-coq:
+	$(BIN) build @runtest-coq
+
 test-all:
-	$(BIN) build @runtest @runtest-js
+	$(BIN) build @runtest @runtest-js @runtest-coq
 
 check:
 	$(BIN) build @check
diff --git a/doc/coq.rst b/doc/coq.rst
new file mode 100644
index 000000000000..a198fe437021
--- /dev/null
+++ b/doc/coq.rst
@@ -0,0 +1,62 @@
+.. _coq-main:
+
+******
+Coq
+******
+
+Dune is also able to build Coq developments. A Coq project is a mix of
+Coq ``.v`` files and (optionally) OCaml libraries (in which case we say the project is a *Coq plugin*). To enable
+Coq support in a dune project, the language version should be selected
+in the ``dune-project`` file. For example:
+
+.. code:: scheme
+
+    (using coq 0.1)
+
+This will enable support for the ``coqlib`` stanza in the current project. If the
+language version is absent, dune will automatically add this line with the
+latest Coq version to the project file once a ``(coqlib ...)`` stanza is used anywhere.
+
+
+Basic Usage
+===========
+
+The basic form for defining Coq libraries is very similar to the OCaml form:
+
+.. code:: scheme
+
+    (coqlib
+     (name <module_prefix>)
+     (synopsis <text>)
+     (modules <ordered_set_lang>)
+     (flags <coq_flags>))
+
+Library Composition and Handling
+===================
+
+The stanza will build all `.v` files on the given directory.
+The semantics of fields is:
+- ``<module_prefix>>`` will be used as the default Coq library prefix
+  ``-R``
+- the ``modules`` field does allow to constraint the set of modules
+  included in the library, similarly to its OCaml counterpart
+- ``<coq_flags>`` will be passed to ``coqc``.
+
+The ``coqlib`` stanza does not yet support composition of Coq
+libraries. In the current version, libraries are located using Coq's
+built-in library management, thus Coq will always resort to the
+installed version of a particular library.
+
+This will be fixed in the future.
+
+Recursive modules
+===================
+
+Adding:
+
+.. code:: scheme
+    (include_subdirs unqualified)
+
+to the ``dune`` will make Dune to consider all the modules in the
+current directory and sub-directories, qualified in the current Coq
+style.
diff --git a/doc/index.rst b/doc/index.rst
index bd04eeecfda3..8cb0e32880db 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -24,6 +24,7 @@ Welcome to dune's documentation!
    jsoo
    variants
    formatting
+   coq
    faq
    known-issues
    migration
diff --git a/src/coq_module.ml b/src/coq_module.ml
new file mode 100644
index 000000000000..2d48ddec256a
--- /dev/null
+++ b/src/coq_module.ml
@@ -0,0 +1,50 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+(* We keep prefix and name separated as the handling of
+  `From Foo Require Bar.` may benefit from it. *)
+type t =
+  { source: Path.t
+  ; prefix : string list
+  ; name : string
+  }
+
+let make ~source ~prefix ~name =
+  { source
+  ; prefix
+  ; name
+  }
+
+let source x = x.source
+let prefix x = x.prefix
+let name x = x.name
+let obj_file ~obj_dir ~ext x =
+  let vo_dir = List.fold_left x.prefix ~init:obj_dir ~f:Path.relative in
+  Path.relative vo_dir (x.name ^ ext)
+let pp fmt x =
+  let open Format in
+  let pp_sep fmt () = pp_print_string fmt "." in
+  fprintf fmt "{ prefix = %a; name = %s; source = %a }"
+    (pp_print_list ~pp_sep pp_print_string) x.prefix x.name Path.pp x.source
+
+let parse ~dir ~loc:_ s =
+  let clist = List.rev @@ String.split s ~on:'.' in
+  match clist with
+  | [] ->
+    Errors.die "invalid coq module"
+  | name :: prefix ->
+    let prefix = List.rev prefix in
+    let source = List.fold_left prefix ~init:dir ~f:Path.relative in
+    let source = Path.relative source (name ^ ".v") in
+    make ~name ~source ~prefix
+
+module Value = struct
+  type nonrec t = t
+  type key = string
+  let key x = String.concat ~sep:"." (x.prefix @ [x.name])
+end
+
+module Eval = Ordered_set_lang.Make(String)(Value)
diff --git a/src/coq_module.mli b/src/coq_module.mli
new file mode 100644
index 000000000000..4605a9b5b56c
--- /dev/null
+++ b/src/coq_module.mli
@@ -0,0 +1,29 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+type t
+
+(** A Coq module [a.b.foo] defined in file [a/b/foo.v] *)
+val make
+  :  source:Path.t
+  (** file = .v source file; module name has to be the same so far *)
+  -> prefix:string list
+  (** Library-local qualified prefix *)
+  -> name:string
+  (** Name of the module *)
+  -> t
+
+(** Coq does enforce some invariants wrt module vs file names *)
+
+val source : t -> Path.t
+val prefix : t -> string list
+val name : t -> string
+val obj_file : obj_dir:Path.t -> ext:string -> t -> Path.t
+val pp : t Fmt.t
+
+(** Parses a form "a.b.c" to a module *)
+val parse : dir:Path.t -> loc:Loc.t -> string -> t
+module Eval : Ordered_set_lang.S with type value := t
diff --git a/src/coq_rules.ml b/src/coq_rules.ml
new file mode 100644
index 000000000000..175862db3d80
--- /dev/null
+++ b/src/coq_rules.ml
@@ -0,0 +1,111 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+open Build.O
+module SC = Super_context
+
+let coq_debug = false
+
+(* TODO:                                       *)
+(* - save library information                  *)
+
+type coq_context =
+  { coqdep : Action.program
+  ; coqc   : Action.program
+  ; coqpp  : Action.program
+  }
+
+let parse_coqdep ~coq_module (lines : string list) =
+  if coq_debug then Format.eprintf "Parsing coqdep @\n%!";
+  let source = Coq_module.source coq_module in
+  let invalid p =
+    Errors.die "coqdep returned invalid output for %s / [phase: %s]"
+      Path.(to_string source) p in
+  let line =
+    match lines with
+    | [] | _ :: _ :: _ :: _ -> invalid "line"
+    | [line] -> line
+    | [l1;_l2] ->
+      (* .vo is produced before .vio, this is fragile tho *)
+      l1
+  in
+  match String.lsplit2 line ~on:':' with
+  | None -> invalid "split"
+  | Some (basename,deps) ->
+    let ff = List.hd @@ String.extract_blank_separated_words basename in
+    let depname, _ext = Filename.(split_extension ff) in
+    let modname =
+      Coq_module.(String.concat ~sep:"/" (prefix coq_module @ [name coq_module])) in
+    if coq_debug
+    then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname;
+    if depname <> modname then invalid "basename";
+    let deps = String.extract_blank_separated_words deps in
+    if coq_debug
+    then Format.eprintf "deps for %a: %a@\n%!" Path.pp source Fmt.(list text) deps;
+    deps
+
+let setup_rule ~expander ~dir ~cc ~source_rule ~name ~cflags coq_module =
+
+  if coq_debug
+  then Format.eprintf "gen_rule coq_module: %a@\n%!" Coq_module.pp coq_module;
+  let obj_dir = dir in
+  let source    = Coq_module.source coq_module in
+  let stdout_to = Coq_module.obj_file ~obj_dir ~ext:".v.d" coq_module in
+  let object_to = Coq_module.obj_file ~obj_dir ~ext:".vo"  coq_module in
+
+  let iflags = Arg_spec.As ["-R"; "."; name] in
+  let cd_arg = Arg_spec.[ iflags; Dep source ] in
+
+  (*  *)
+  let coqdep_rule =
+    source_rule >>>
+    Build.(run ~dir ~stdout_to cc.coqdep cd_arg)
+  in
+
+  (* Process coqdep and generate rules *)
+  let deps_of = Build.dyn_paths (
+    Build.lines_of stdout_to >>^
+    parse_coqdep ~coq_module >>^
+    List.map ~f:Path.(relative dir)
+  ) in
+  let cc_arg = Arg_spec.[
+    iflags;
+    Dep source;
+    Hidden_targets [object_to] ]
+  in
+  [coqdep_rule;
+   deps_of >>>
+   Expander.expand_and_eval_set expander cflags ~standard:Build.(return []) >>>
+   Build.run ~dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg)
+  ]
+
+let create_ccoq sctx ~dir =
+  let rr prg =
+    SC.resolve_program ~dir sctx prg ~loc:None ~hint:"try: opam install coq" in
+  { coqdep = rr "coqdep"
+  ; coqc   = rr "coqc"
+  ; coqpp  = rr "coqpp"
+  }
+
+let setup_rules ~sctx ~dir ~dir_contents ~scope (s : Dune_file.Coq.t) =
+
+  if coq_debug then
+    Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!"
+      Path.pp dir Path.pp Scope.(root scope)
+  ;
+
+  let cc = create_ccoq sctx ~dir in
+  let name = snd s.name in
+  let coq_modules = Dir_contents.coq_modules_of_library dir_contents ~name in
+
+  (* coqdep requires all the files to be in the tree to produce correct
+     dependencies *)
+  let source_rule = Build.paths List.(map ~f:Coq_module.source coq_modules) in
+  let cflags = s.Dune_file.Coq.flags in
+  let expander = SC.expander sctx ~dir in
+  let coq_rules =
+    List.concat_map
+      ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~name ~cflags) coq_modules in
+  coq_rules
diff --git a/src/coq_rules.mli b/src/coq_rules.mli
new file mode 100644
index 000000000000..6ed39c367586
--- /dev/null
+++ b/src/coq_rules.mli
@@ -0,0 +1,15 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+(* Build rules for Coq's .v -> .vo files       *)
+
+open! Stdune
+
+val setup_rules
+  :  sctx:Super_context.t
+  -> dir:Path.t
+  -> dir_contents:Dir_contents.t
+  -> scope:Scope.t
+  -> Dune_file.Coq.t
+  -> (unit, Action.t) Build.t list
diff --git a/src/dir_contents.ml b/src/dir_contents.ml
index 723f1dc474a8..3a18a9b0cefe 100644
--- a/src/dir_contents.ml
+++ b/src/dir_contents.ml
@@ -180,6 +180,7 @@ type t =
   ; modules : Modules.t Lazy.t
   ; c_sources : C_sources.t Lazy.t
   ; mlds : (Dune_file.Documentation.t * Path.t list) list Lazy.t
+  ; coq_modules : Coq_module.t list String.Map.t Lazy.t
   }
 
 and kind =
@@ -239,6 +240,16 @@ let mlds t (doc : Documentation.t) =
                        (List.map map ~f:(fun (d, _) -> d.Documentation.loc))
       ]
 
+let coq_modules_of_library t ~name =
+  let map = Lazy.force t.coq_modules in
+  match String.Map.find map name with
+  | Some x -> x
+  | None ->
+    Exn.code_error "Dir_contents.coq_modules_of_library"
+      [ "name", Sexp.Encoder.string name
+      ; "available", Sexp.Encoder.(list string) (String.Map.keys map)
+      ]
+
 (* As a side-effect, setup user rules and copy_files rules. *)
 let load_text_files sctx ft_dir
       { Dir_with_dune.
@@ -255,6 +266,10 @@ let load_text_files sctx ft_dir
   let generated_files =
     List.concat_map stanzas ~f:(fun stanza ->
       match (stanza : Stanza.t) with
+      | Coq.T _coq ->
+        (* Format.eprintf "[coq] generated_files called at sctx: %a@\n%!" Path.pp File_tree.Dir.(path ft_dir); *)
+        (* FIXME: Need to generate ml files from mlg ? *)
+        []
       | Menhir.T menhir ->
         Menhir_rules.targets menhir
       | Rule rule ->
@@ -338,6 +353,28 @@ let build_mlds_map (d : _ Dir_with_dune.t) ~files =
       Some (doc, List.map (String.Map.values mlds) ~f:(Path.relative dir))
     | _ -> None)
 
+let coq_modules_of_files ~subdirs =
+  let filter_v_files (dir, local, files) =
+    (dir, local, String.Set.filter files ~f:(fun f -> Filename.check_suffix f ".v")) in
+  let subdirs = List.map subdirs ~f:filter_v_files in
+  let build_mod_dir (dir, prefix, files) =
+    String.Set.to_list files |> List.map ~f:(fun file ->
+      let name, _ = Filename.split_extension file in
+      Coq_module.make ~source:Path.(relative dir file) ~prefix ~name) in
+  let modules = List.concat_map ~f:build_mod_dir subdirs in
+  modules
+
+(* TODO: Build reverse map and check duplicates, however, are duplicates harmful?
+ * In Coq all libs are "wrapped" so including a module twice is not so bad.
+ *)
+let build_coq_modules_map (d : _ Dir_with_dune.t) ~dir ~modules =
+  List.fold_left d.data ~init:String.Map.empty ~f:(fun map -> function
+    | Coq.T coq ->
+      let modules = Coq_module.Eval.eval coq.modules
+        ~parse:Coq_module.(parse ~dir) ~standard:modules in
+      String.Map.add map (snd coq.name) modules
+    | _ -> map)
+
 let cache = Hashtbl.create 32
 
 let clear_cache () =
@@ -367,6 +404,9 @@ let rec get sctx ~dir =
               C_sources.make d
                 ~c_sources:(C_sources.load_sources ~dune_version ~dir:d.ctx_dir
                               ~files))
+          ; coq_modules =
+              lazy (build_coq_modules_map d ~dir:d.ctx_dir
+                      ~modules:(coq_modules_of_files ~subdirs:[dir,[],files]))
           }
         | Some (_, None)
         | None ->
@@ -376,6 +416,7 @@ let rec get sctx ~dir =
           ; modules = lazy Modules.empty
           ; mlds = lazy []
           ; c_sources = lazy C_sources.empty
+          ; coq_modules = lazy String.Map.empty
           }
       in
       Hashtbl.add cache dir t;
@@ -389,7 +430,7 @@ let rec get sctx ~dir =
           Hashtbl.find_exn cache dir
       end
     | Group_root (ft_dir, d) ->
-      let rec walk ft_dir ~dir acc =
+      let rec walk ft_dir ~dir ~local acc =
         match
           Dir_status.DB.get dir_status_db ~dir
         with
@@ -399,20 +440,21 @@ let rec get sctx ~dir =
             | None -> File_tree.Dir.files ft_dir
             | Some d -> load_text_files sctx ft_dir d
           in
-          walk_children ft_dir ~dir ((dir, files) :: acc)
+          walk_children ft_dir ~dir ~local ((dir, local, files) :: acc)
         | _ -> acc
-      and walk_children ft_dir ~dir acc =
+      and walk_children ft_dir ~dir ~local acc =
         String.Map.foldi (File_tree.Dir.sub_dirs ft_dir) ~init:acc
           ~f:(fun name ft_dir acc ->
             let dir = Path.relative dir name in
-            walk ft_dir ~dir acc)
+            let local = local @ [name] in
+            walk ft_dir ~dir ~local acc)
       in
       let files = load_text_files sctx ft_dir d in
-      let subdirs = walk_children ft_dir ~dir [] in
+      let subdirs = walk_children ft_dir ~dir ~local:[] [] in
       let modules = lazy (
         let modules =
-          List.fold_left ((dir, files) :: subdirs) ~init:Module.Name.Map.empty
-            ~f:(fun acc (dir, files) ->
+          List.fold_left ((dir, [], files) :: subdirs) ~init:Module.Name.Map.empty
+            ~f:(fun acc (dir, _, files) ->
               let modules = modules_of_files ~dir ~files in
               Module.Name.Map.union acc modules ~f:(fun name x y ->
                 Errors.fail (Loc.in_file
@@ -434,8 +476,8 @@ let rec get sctx ~dir =
         let dune_version = d.dune_version in
         let init = C.Kind.Dict.make String.Map.empty in
         let c_sources =
-          List.fold_left ((dir, files) :: subdirs) ~init
-            ~f:(fun acc (dir, files) ->
+          List.fold_left ((dir, [], files) :: subdirs) ~init
+            ~f:(fun acc (dir, _, files) ->
               let sources = C_sources.load_sources ~dir ~dune_version ~files in
               let f acc sources =
                 String.Map.union acc sources ~f:(fun name x y ->
@@ -458,18 +500,23 @@ let rec get sctx ~dir =
         in
         C_sources.make d ~c_sources
       ) in
+      let coq_modules = lazy (
+        build_coq_modules_map d ~dir:d.ctx_dir
+          ~modules:(coq_modules_of_files ~subdirs:((dir,[],files)::subdirs))
+      ) in
       let t =
         { kind = Group_root
-                   (lazy (List.map subdirs ~f:(fun (dir, _) -> get sctx ~dir)))
+                   (lazy (List.map subdirs ~f:(fun (dir, _, _) -> get sctx ~dir)))
         ; dir
         ; text_files = files
         ; modules
         ; c_sources
         ; mlds = lazy (build_mlds_map d ~files)
+        ; coq_modules
         }
       in
       Hashtbl.add cache dir t;
-      List.iter subdirs ~f:(fun (dir, files) ->
+      List.iter subdirs ~f:(fun (dir, _local, files) ->
         Hashtbl.add cache dir
           { kind = Group_part t
           ; dir
@@ -477,5 +524,6 @@ let rec get sctx ~dir =
           ; modules
           ; c_sources
           ; mlds = lazy (build_mlds_map d ~files)
+          ; coq_modules
           });
       t
diff --git a/src/dir_contents.mli b/src/dir_contents.mli
index 7c466c7abea2..cabb1782f220 100644
--- a/src/dir_contents.mli
+++ b/src/dir_contents.mli
@@ -34,6 +34,9 @@ val lookup_module : t -> Module.Name.t -> Dune_file.Buildable.t option
 (** All mld files attached to this documentation stanza *)
 val mlds : t -> Dune_file.Documentation.t -> Path.t list
 
+(** Coq modules of library [name] is the Coq library name.  *)
+val coq_modules_of_library : t -> name:string -> Coq_module.t list
+
 val get : Super_context.t -> dir:Path.t -> t
 
 type kind = private
diff --git a/src/dune_file.ml b/src/dune_file.ml
index d4b261d55ce8..5979cd57c64c 100644
--- a/src/dune_file.ml
+++ b/src/dune_file.ml
@@ -1788,6 +1788,60 @@ module Menhir = struct
        })
 end
 
+module Coq = struct
+
+  type t =
+    (* ; public     : Public_lib.t option *\) *)
+    { name       : Loc.t * string
+    (* TODO: validate name *)
+    ; synopsis   : string option
+    ; modules    : Ordered_set_lang.t
+    ; flags      : Ordered_set_lang.Unexpanded.t
+    ; libraries  : Lib_dep.t list
+    (** ocaml libraries *)
+    ; loc        : Loc.t
+    ; enabled_if : Blang.t
+    }
+
+  let syntax =
+    Syntax.create
+      ~name:"coq"
+      ~desc:"the coq extension (experimental)"
+      [ 0, 1 ]
+
+  let decode =
+    record
+      (* let_map name = field_o "name" Lib_name.Local.decode_loc
+       * and public = Public_lib.public_name_field *)
+      (let+ name = field "name" (located string)
+       and+ loc = loc
+       and+ synopsis = field_o "synopsis" string
+       and+ flags = field_oslu "flags"
+       and+ modules = modules_field "modules"
+       and+ libraries = field "libraries" Lib_deps.decode ~default:[]
+       and+ enabled_if = enabled_if
+       in
+       (* { name
+        * ; public *)
+       { name
+       ; synopsis
+       ; modules
+       ; flags
+       ; libraries
+       ; loc
+       ; enabled_if
+       })
+
+  type Stanza.t += T of t
+
+  let () =
+    Dune_project.Extension.register_simple
+      syntax
+      (return [ "coqlib", decode >>| fun x -> [T x] ])
+
+end
+
+
 module Alias_conf = struct
   type t =
     { name    : string
diff --git a/src/dune_file.mli b/src/dune_file.mli
index 0f2b4ed3c1c5..f90a0fb13124 100644
--- a/src/dune_file.mli
+++ b/src/dune_file.mli
@@ -353,6 +353,23 @@ module Menhir : sig
   type Stanza.t += T of t
 end
 
+module Coq : sig
+
+  type t =
+    (* ; public     : Public_lib.t option *\) *)
+    { name       : Loc.t * string
+    ; synopsis   : string option
+    ; modules    : Ordered_set_lang.t
+    ; flags      : Ordered_set_lang.Unexpanded.t
+    ; libraries  : Lib_dep.t list
+    (** ocaml libraries *)
+    ; loc        : Loc.t
+    ; enabled_if : Blang.t
+    }
+
+  type Stanza.t += T of t
+end
+
 module Alias_conf : sig
   type t =
     { name    : string
diff --git a/src/gen_rules.ml b/src/gen_rules.ml
index 155846ef3607..e6264a48d34d 100644
--- a/src/gen_rules.ml
+++ b/src/gen_rules.ml
@@ -185,6 +185,11 @@ module Gen(P : sig val sctx : Super_context.t end) = struct
         | Some cctx ->
           Menhir_rules.gen_rules cctx m ~dir:ctx_dir
         end
+      | Coq.T m when Expander.eval_blang expander m.enabled_if ->
+        (* Format.eprintf "[coq] gen_rules called @\n%!"; *)
+        let dir = ctx_dir in
+        let coq_rules = Coq_rules.setup_rules ~sctx ~dir ~scope ~dir_contents m in
+        SC.add_rules ~dir:ctx_dir sctx coq_rules
       | _ -> ());
     let dyn_deps =
       let pred =
diff --git a/src/stdune/option.ml b/src/stdune/option.ml
index 16a05bff6be6..f076ef01dfaf 100644
--- a/src/stdune/option.ml
+++ b/src/stdune/option.ml
@@ -39,6 +39,11 @@ let value_exn = function
   | Some x -> x
   | None -> Exn.code_error "Option.value_exn" []
 
+let value_map t ~f ~default =
+  match t with
+  | Some x -> f x
+  | None -> default
+
 let some x = Some x
 
 let some_if cond x =
diff --git a/src/stdune/option.mli b/src/stdune/option.mli
index d32a34792758..6a304e5c3e87 100644
--- a/src/stdune/option.mli
+++ b/src/stdune/option.mli
@@ -22,6 +22,8 @@ val forall: 'a t -> f:('a -> bool) -> bool
 val value : 'a t -> default:'a -> 'a
 val value_exn : 'a t -> 'a
 
+val value_map : 'a t -> f:('a -> 'b) -> default:'b -> 'b
+
 val some : 'a -> 'a t
 val some_if : bool -> 'a -> 'a t
 
diff --git a/test/blackbox-tests/dune.inc b/test/blackbox-tests/dune.inc
index 993efd5e108b..40a531075d52 100644
--- a/test/blackbox-tests/dune.inc
+++ b/test/blackbox-tests/dune.inc
@@ -95,6 +95,14 @@
    test-cases/copy_files
    (progn (run %{exe:cram.exe} -test run.t) (diff? run.t run.t.corrected)))))
 
+(alias
+ (name coq)
+ (deps (package dune) (source_tree test-cases/coq))
+ (action
+  (chdir
+   test-cases/coq
+   (progn (run %{exe:cram.exe} -test run.t) (diff? run.t run.t.corrected)))))
+
 (alias
  (name cross-compilation)
  (deps (package dune) (source_tree test-cases/cross-compilation))
@@ -1625,4 +1633,6 @@
 
 (alias (name runtest-disabled) (deps (alias envs-and-contexts)))
 
-(alias (name runtest-js) (deps (alias js_of_ocaml)))
\ No newline at end of file
+(alias (name runtest-js) (deps (alias js_of_ocaml)))
+
+(alias (name runtest-coq) (deps (alias coq)))
\ No newline at end of file
diff --git a/test/blackbox-tests/gen_tests.ml b/test/blackbox-tests/gen_tests.ml
index d8aca4fab120..d753339260b4 100644
--- a/test/blackbox-tests/gen_tests.ml
+++ b/test/blackbox-tests/gen_tests.ml
@@ -61,10 +61,11 @@ module Test = struct
     ; skip_platforms : Platform.t list
     ; enabled        : bool
     ; js             : bool
+    ; coq            : bool
     ; external_deps  : bool
     }
 
-  let make ?env ?skip_ocaml ?(skip_platforms=[]) ?(enabled=true) ?(js=false)
+  let make ?env ?skip_ocaml ?(skip_platforms=[]) ?(enabled=true) ?(js=false) ?(coq=false)
         ?(external_deps=false) name =
     { name
     ; env
@@ -73,6 +74,7 @@ module Test = struct
     ; external_deps
     ; enabled
     ; js
+    ; coq
     }
 
   let pp_sexp fmt t =
@@ -123,6 +125,7 @@ let exclusions =
   let odoc = make ~external_deps:true ~skip_ocaml:"4.02.3" in
   [ make "js_of_ocaml" ~external_deps:true ~js:true
       ~env:("NODE", Sexp.parse "%{bin:node}")
+  ; make "coq" ~external_deps:true ~coq:true
   ; make "github25" ~env:("OCAMLPATH", Dune_lang.atom "./findlib-packages")
   ; odoc "odoc"
   ; odoc "odoc-unique-mlds"
@@ -179,13 +182,14 @@ let pp_group fmt (name, tests) =
 
 let () =
   let tests = Lazy.force all_tests in
-  (* The runtest target has a "specoial" definition. It includes all tests
-     except for js and disabled tests *)
+  (* The runtest target has a "special" definition. It includes all
+     tests except for js, coq, and disabled tests *)
   tests |> List.iter ~f:(fun t -> Format.printf "%a@.@." Test.pp_sexp t);
-  [ "runtest", (fun (t : Test.t) -> not t.js && t.enabled)
+  [ "runtest", (fun (t : Test.t) -> not t.js && not t.coq && t.enabled)
   ; "runtest-no-deps", (fun (t : Test.t) -> not t.external_deps && t.enabled)
   ; "runtest-disabled", (fun (t : Test.t) -> not t.enabled)
-  ; "runtest-js", (fun (t : Test.t) -> t.js && t.enabled) ]
+  ; "runtest-js", (fun (t : Test.t) -> t.js && t.enabled)
+  ; "runtest-coq", (fun (t : Test.t) -> t.coq && t.enabled) ]
   |> List.map ~f:(fun (name, predicate) ->
     (name, List.filter tests ~f:predicate))
   |> Format.pp_print_list
diff --git a/test/blackbox-tests/test-cases/coq/base/bar.v b/test/blackbox-tests/test-cases/coq/base/bar.v
new file mode 100644
index 000000000000..4627b76131c1
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/base/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/base/dune b/test/blackbox-tests/test-cases/coq/base/dune
new file mode 100644
index 000000000000..be9cdd1880b8
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/base/dune
@@ -0,0 +1,5 @@
+(coqlib
+ (name basic)
+ ; (public_name dune.test.basic)
+ (modules)
+ (synopsis "Test Coq library"))
diff --git a/test/blackbox-tests/test-cases/coq/base/dune-project b/test/blackbox-tests/test-cases/coq/base/dune-project
new file mode 100644
index 000000000000..0f1c4e5f17f9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/base/dune-project
@@ -0,0 +1,3 @@
+(lang dune 1.4)
+
+(using coq 0.1)
diff --git a/test/blackbox-tests/test-cases/coq/base/foo.v b/test/blackbox-tests/test-cases/coq/base/foo.v
new file mode 100644
index 000000000000..53e0ce1b1526
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/base/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v b/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v
new file mode 100644
index 000000000000..b1e4f474ced9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v
@@ -0,0 +1,5 @@
+From rec_module Require Import b.foo.
+From rec_module Require Import c.ooo.
+From rec_module Require c.d.bar.
+
+Definition mynum (i : mynat) := 3 + ooo_nat + c.d.bar.bar_nat.
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v b/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v
new file mode 100644
index 000000000000..53e0ce1b1526
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v
@@ -0,0 +1 @@
+Definition mynat := nat.
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v b/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v
new file mode 100644
index 000000000000..b68bd7244fba
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v
@@ -0,0 +1 @@
+Definition bar_nat : nat := 4.
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v b/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v
new file mode 100644
index 000000000000..07d40e567986
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v
@@ -0,0 +1 @@
+Definition ooo_nat : nat := 10.
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/dune b/test/blackbox-tests/test-cases/coq/rec_module/dune
new file mode 100644
index 000000000000..8c8b5efe8661
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/dune
@@ -0,0 +1,7 @@
+(coqlib
+ (name rec_module)
+ ; (public_name dune.test.basic)
+ (modules :standard)
+ (synopsis "Test Coq library"))
+
+(include_subdirs unqualified)
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/dune-project b/test/blackbox-tests/test-cases/coq/rec_module/dune-project
new file mode 100644
index 000000000000..0f1c4e5f17f9
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/rec_module/dune-project
@@ -0,0 +1,3 @@
+(lang dune 1.4)
+
+(using coq 0.1)
diff --git a/test/blackbox-tests/test-cases/coq/run.t b/test/blackbox-tests/test-cases/coq/run.t
new file mode 100644
index 000000000000..de134a1dcf70
--- /dev/null
+++ b/test/blackbox-tests/test-cases/coq/run.t
@@ -0,0 +1,5 @@
+  $ dune build --root base --display short --debug-dependency-path @all
+  Entering directory 'base'
+
+  $ dune build --root rec_module --display short --debug-dependency-path @all
+  Entering directory 'rec_module'