[dune] [stdlib] Build the standard library natively with Dune.

This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?

1 files changed, 1 insertions, 6 deletions

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0506216541..8b0bf216e3 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-If you want to build the standard libraries and plugins you should
-call `make -f Makefile.dune voboot`. It is usually enough to do that
-once per-session.
-
 More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
@@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and
 `coqide` in a fast build. In order to use them, do:
 
 ```
-$ make -f Makefile.dune voboot                # Only once per session
 $ dune exec -- dev/shim/coqtop-prelude
 ```
 
@@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors:
 
 ## Dropping from coqtop:
 
-After doing `make -f Makefile.dune voboot`, the following commands should work:
+The following commands should work:
 ```
 dune exec -- dev/shim/coqbyte-prelude
 > Drop.