; This is an ad-hoc rule to ease the migration, it should be handled
; natively by Dune in the future.
(rule
 (targets index-list.html)
 (deps
   make-library-index index-list.html.template hidden-files
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/user-contrib))
 (action
  (chdir %{project_root}
   ; On windows run will fail
   (bash "doc/corelib/make-library-index doc/corelib/index-list.html doc/corelib/hidden-files"))))

(rule
  (targets (dir html))
  (alias corelib-html)
  (deps
   ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/user-contrib)
   (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
   (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
   ; For .glob files, should be gone when Coq Dune is smarter.
   (package rocq-runtime)
   (package coq-core)
   (package rocq-core))
 (action
  (progn
   (run mkdir -p html)
   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories/Corelib Corelib -Q %{project_root}/theories/Ltac2 Ltac2 $(find %{project_root}/theories -name *.v)")
   (run mv html/index.html html/genindex.html)
   (with-stdout-to
     _index.html
    (progn (bash "sed 's/@@TITLE@@/Table of contents/' %{header}")
     (cat index-list.html)
     (cat %{footer})))
   (run cp _index.html html/index.html))))