[travis] Enable Coq tests [using OPAM]

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

.travis-ci.sh

@@ -94,14 +94,15 @@ case "$TARGET" in
       fi
       opam list
       opam pin add dune . --no-action
-      opam install ocamlfind utop ppxlib $ODOC ocaml-migrate-parsetree js_of_ocaml-ppx js_of_ocaml-compiler
+      opam install ocamlfind utop ppxlib $ODOC ocaml-migrate-parsetree js_of_ocaml-ppx js_of_ocaml-compiler coq
       echo -en "travis_fold:end:opam.deps\r"
     fi
     echo -en "travis_fold:end:dune.boot\r"
     if [ $WITH_OPAM -eq 1 ] ; then
       cat $RUNTEST_NO_DEPS;
       _boot/install/default/bin/dune runtest && \
       _boot/install/default/bin/dune build @test/blackbox-tests/runtest-js && \
+      _boot/install/default/bin/dune build @test/blackbox-tests/runtest-coq && \
       ! _boot/install/default/bin/dune build @test/fail-with-background-jobs-running
       RESULT=$?
       if [ $UPDATE_OPAM -eq 0 ] ; then

src/dune_file.ml

@@ -1865,10 +1865,14 @@ module Coq = struct
 
   type Stanza.t += T of t
 
-  let () =
-    Dune_project.Extension.register_simple
-      syntax
-      (return [ "coqlib", decode >>| fun x -> [T x] ])
+  let unit_to_sexp () = Sexp.List []
+
+  let unit_stanzas =
+    let+ r = return ["coqlib", decode >>| fun x -> [T x]] in
+    ((), r)
+
+  let key =
+    Dune_project.Extension.register syntax unit_stanzas unit_to_sexp
 
 end
 
@@ -2110,8 +2114,12 @@ module Stanzas = struct
       (let+ x = Dune_env.Stanza.decode in
        [Dune_env.T x])
     ; "include_subdirs",
-      (let+ () = Syntax.since Stanza.syntax (1, 1)
-       and+ t = Include_subdirs.decode ~enable_qualified:false
+      (Dune_project.get_exn () >>= fun p ->
+       let+ () = Syntax.since Stanza.syntax (1, 1)
+       and+ t =
+         let enable_qualified =
+           Option.is_some (Dune_project.find_extension_args p Coq.key) in
+         Include_subdirs.decode ~enable_qualified
        and+ loc = loc in
        [Include_subdirs (loc, t)])
     ; "toplevel",