2 files changed, 41 insertions, 4 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 9d10a8ba72..e370d37fc4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
-let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let sigma = Evd.minimize_universes sigma in
   let body = EConstr.to_constr sigma body in
   let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
@@ -9,16 +9,17 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
      (Option.List.cons tyopt [body]) in
   let sigma = Evd.restrict_universe_context sigma uvars in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ident k ce ubinders imps ~hook
+  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  let nohook = Lemmas.mk_hook (fun _ x -> ()) in
-  ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
new file mode 100644
index 0000000000..7fe2493fbf
--- /dev/null
+++ b/doc/stdlib/dune
@@ -0,0 +1,36 @@
+; 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}/plugins))
+ (action
+  (chdir %{project_root}
+   ; On windows run will fail
+   (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files"))))
+
+(rule
+  (targets html)
+  (deps
+   ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
+   (source_tree %{project_root}/theories)
+   (source_tree %{project_root}/plugins)
+   (: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 coq))
+ (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 Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
+   (run mv html/index.html html/genindex.html)
+   (with-stdout-to
+     _index.html
+    (progn (cat %{header}) (cat index-list.html) (cat %{footer})))
+   (run cp _index.html html/index.html))))
+
+(alias
+ (name stdlib-html)
+ (deps html))