3 files changed, 47 insertions, 3 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index da91c85856..a31ab1c511 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -44,6 +44,24 @@ Dune will read the file `~/.config/dune/config`; see `man
 dune-config`. Among others, you can set in this file the custom number
 of build threads `(jobs N)` and display options `(display _mode_)`.
 
+## Running binaries [coqtop / coqide]
+
+There are two special targets `states` and `quickide` that will
+generate "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
+```
+
+or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
+enjoy quick incremental compilation thanks to `-opaque` so they tend
+to be very fast while developing.
+
+Note that for a fast developer build of ML files, the `check` target
+will be faster.
+
 ## Targets
 
 The default dune target is `dune build` (or `dune build @install`),
diff --git a/dev/shim/dune b/dev/shim/dune
new file mode 100644
index 0000000000..85a0d205da
--- /dev/null
+++ b/dev/shim/dune
@@ -0,0 +1,27 @@
+(rule
+ (targets coqtop-prelude)
+ (deps
+  %{bin:coqtop}
+  %{project_root}/theories/Init/Prelude.vo)
+ (action
+  (with-outputs-to coqtop-prelude
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
+
+(rule
+ (targets coqide-prelude)
+ (deps
+  %{bin:coqqueryworker.opt}
+  %{bin:coqtacticworker.opt}
+  %{bin:coqproofworker.opt}
+  %{project_root}/theories/Init/Prelude.vo
+  %{project_root}/coqide-server.install
+  %{project_root}/coqide.install)
+ (action
+  (with-outputs-to coqide-prelude
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index ec72f96509..c6687b9731 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -80,9 +80,8 @@ Note that this function is executed before _Coqproject is read if it exists."
     (when dir
       (unless coq-prog-args
         (setq coq-prog-args
-              `("-coqlib" ,dir "-R" ,(concat dir "plugins")
-                "Coq" "-R" ,(concat dir "theories")
-                "Coq")))
+              `("-coqlib" ,dir
+                "-topfile" ,buffer-file-name)))
       (setq-local coq-prog-name (concat dir "bin/coqtop")))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)