[dev] Add include versions for Dune builds.

Fixes #9537

This way, users can do:
```
dune exec coqtop.byte
> Drop.
 # #directory "dev";;
 # #use "include_dune";;
```

9 files changed, 136 insertions, 90 deletions

diff --git a/dev/base_include b/dev/base_include
index 48feeec147..b214959bad 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -1,24 +1,6 @@
-
 (* File to include to get some Coq facilities under the ocaml toplevel.
    This file is loaded by include *)
 
-#cd".";;
-#directory "parsing";;
-#directory "interp";;
-#directory "toplevel";;
-#directory "library";;
-#directory "kernel";;
-#directory "gramlib";;
-#directory "engine";;
-#directory "pretyping";;
-#directory "lib";;
-#directory "proofs";;
-#directory "tactics";;
-#directory "printing";;
-#directory "grammar";;
-#directory "stm";;
-#directory "vernac";;
-
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -137,7 +119,6 @@ open Proof_global
 open Redexpr
 open Refiner
 open Tacmach
-open Tactic_debug
 
 open Hints
 open Auto
@@ -146,15 +127,9 @@ open Contradiction
 open Eauto
 open Elim
 open Equality
-open Evar_tactics
-open Extraargs
-open Extratactics
 open Hipattern
 open Inv
 open Leminv
-open Tacsubst
-open Tacintern
-open Tacinterp
 open Tacticals
 open Tactics
 open Eqschemes
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 01c32041d2..da91c85856 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -106,6 +106,16 @@ refined, so you need to build enough of Coq once to use this target
 [it will then correctly compute the deps and rebuild if you call the
 script again] This will be fixed in the future.
 
+## Dropping from coqtop:
+
+The following sequence is recommended:
+```
+dune exec coqtop.byte
+> Drop.
+# #directory "dev";;
+# #use "include_dune";;
+```
+
 ## Compositionality, developer and release modes.
 
 By default [in "developer mode"], Dune will compose all the packages
diff --git a/dev/inc_ltac b/dev/inc_ltac
new file mode 100644
index 0000000000..8ef02445c2
--- /dev/null
+++ b/dev/inc_ltac
@@ -0,0 +1,7 @@
+open Evar_tactics
+open Tactic_debug
+open Tacsubst
+open Tacintern
+open Tacinterp
+open Extraargs
+open Extratactics
diff --git a/dev/inc_ltac_dune b/dev/inc_ltac_dune
new file mode 100644
index 0000000000..d7f505e8e0
--- /dev/null
+++ b/dev/inc_ltac_dune
@@ -0,0 +1,7 @@
+open Ltac_plugin__Evar_tactics
+open Ltac_plugin__Tactic_debug
+open Ltac_plugin__Tacsubst
+open Ltac_plugin__Tacintern
+open Ltac_plugin__Tacinterp
+open Ltac_plugin__Extraargs
+open Ltac_plugin__Extratactics
diff --git a/dev/incdir b/dev/incdir
new file mode 100644
index 0000000000..8ffd6bf6dc
--- /dev/null
+++ b/dev/incdir
@@ -0,0 +1,16 @@
+#cd".";;
+#directory "parsing";;
+#directory "interp";;
+#directory "toplevel";;
+#directory "library";;
+#directory "kernel";;
+#directory "gramlib";;
+#directory "engine";;
+#directory "pretyping";;
+#directory "lib";;
+#directory "proofs";;
+#directory "tactics";;
+#directory "printing";;
+#directory "grammar";;
+#directory "stm";;
+#directory "vernac";;
diff --git a/dev/incdir_dune b/dev/incdir_dune
new file mode 100644
index 0000000000..9d0fee1fa2
--- /dev/null
+++ b/dev/incdir_dune
@@ -0,0 +1,16 @@
+#cd".";;
+#directory "_build/default/lib/.lib.objs/";;
+#directory "_build/default/clib/.clib.objs/";;
+#directory "_build/default/kernel/.kernel.objs/";;
+#directory "_build/default/library/.library.objs/";;
+#directory "_build/default/engine/.engine.objs/";;
+#directory "_build/default/pretyping/.pretyping.objs/";;
+#directory "_build/default/interp/.interp.objs/";;
+#directory "_build/default/parsing/.parsing.objs/";;
+#directory "_build/default/gramlib/.gramlib.objs/";;
+#directory "_build/default/proofs/.proofs.objs/";;
+#directory "_build/default/tactics/.tactics.objs/";;
+#directory "_build/default/printing/.printing.objs/";;
+#directory "_build/default/vernac/.vernac.objs/";;
+#directory "_build/default/stm/.stm.objs/";;
+#directory "_build/default/toplevel/.toplevel.objs/";;
diff --git a/dev/include b/dev/include
index c5de83b900..fa4bf827d7 100644
--- a/dev/include
+++ b/dev/include
@@ -1,4 +1,3 @@
-
 (* File to include to install the pretty-printers in the ocaml toplevel *)
 
 (* Typical usage :
@@ -15,69 +14,8 @@
    then ignore (Toploop.use_silently Format.std_formatter "dev/include")
 *)
 
-(* For OCaml 3.10.x:
-   clflags.cmi (a ocaml compilation by-product) must be in the library path.
-   On Debian, install ocaml-compiler-libs, and uncomment the following:
-   #directory "+compiler-libs/utils";;
-   Clflags.recursive_types := true;;
-*)
-
 #cd ".";;
+#use "incdir";;
 #use "base_include";;
-
-#install_printer  (* pp_stdcmds *) pp;;
-
-#install_printer  (* pattern *) pppattern;;
-#install_printer  (* glob_constr *) ppglob_constr;;
-#install_printer  (* open constr *) ppopenconstr;;
-#install_printer  (* constr *) ppconstr;;
-#install_printer  (* econstr *) ppeconstr;;
-#install_printer  (* constr_substituted *) ppsconstr;; 
-#install_printer  (* constraints *)  ppconstraints;;
-#install_printer  (* univ constraints *)  ppuniverseconstraints;;
-#install_printer  (* universe *)  ppuni;;
-#install_printer  (* universes *)  ppuniverses;;
-#install_printer  (* univ level *) ppuni_level;;
-#install_printer  (* univ context *) ppuniverse_context;;
-#install_printer  (* univ context future *) ppuniverse_context_future;;
-#install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ set *) ppuniverse_set;;
-#install_printer  (* univ instance *) ppuniverse_instance;;
-#install_printer  (* univ subst *) ppuniverse_subst;;
-#install_printer  (* univ full subst *) ppuniverse_level_subst;;
-#install_printer  (* univ opt subst *) ppuniverse_opt_subst;;
-#install_printer  (* evar univ ctx *) ppevar_universe_context;;
-#install_printer  (* inductive *) ppind;;
-#install_printer  (* 'a scheme_kind *) ppscheme;;
-#install_printer  (* type_judgement *) pptype;;
-#install_printer  (* judgement *) ppj;;
-#install_printer  (* id set *) ppidset;;
-#install_printer  (* int set *) ppintset;;
-
-#install_printer  (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
-#install_printer  (* Reductionops machine stack *) pp_stack_t;;
-
-(*#install_printer  (* hint_db *)  print_hint_db;;*)
-(*#install_printer  (* hints_path *)  pphintspath;;*)
-#install_printer  (* goal *)  ppgoal;;
-(*#install_printer  (* sigma goal *)  ppsigmagoal;;*)
-#install_printer  (* proof *)  pproof;;
-#install_printer  (* Goal.goal *)  ppgoalgoal;;
-#install_printer  (* proofview *)  ppproofview;;
-#install_printer  (* metaset.t *) ppmetas;;
-#install_printer  (* evar *)  ppevar;;
-#install_printer  (* evar_map *)  ppevm;;
-#install_printer  (* Evar.Set.t *) ppexistentialset;;
-#install_printer  (* clenv *) ppclenv;;
-#install_printer  (* env *) ppenv;;
-#install_printer  (* Hint_db.t *) pphintdb;;
-#install_printer  (* named_context_val *) ppnamedcontextval;;
-
-#install_printer  (* tactic *) pptac;;
-#install_printer  (* object *) ppobj;;
-#install_printer  (* global_reference *) ppglobal;;
-#install_printer  (* generic_argument *) pp_generic_argument;;
-
-#install_printer  (* fconstr *) ppfconstr;;
-
-#install_printer (* Future.computation *) ppfuture;;
+#use "inc_ltac";;
+#use "include_printers";;
diff --git a/dev/include_dune b/dev/include_dune
new file mode 100644
index 0000000000..2ef8eb4d04
--- /dev/null
+++ b/dev/include_dune
@@ -0,0 +1,22 @@
+(* File to include to install the pretty-printers in the ocaml toplevel *)
+
+(* Typical usage :
+
+   $ dune exec coqtop.byte # or even better : rlwrap coqtop.byte
+   Coq < Drop.
+   # #directory "dev";;
+   # #use "include";;
+
+   Alternatively, you can avoid typing #use "include" after each Drop
+   by adding the following lines in your $HOME/.ocamlinit :
+
+   #directory "+compiler-libs";;
+   if Filename.basename Sys.argv.(0) = "coqtop.byte"
+   then ignore (Toploop.use_silently Format.std_formatter "dev/include")
+*)
+
+#cd ".";;
+#use "incdir_dune";;
+#use "base_include";;
+#use "inc_ltac_dune";;
+#use "include_printers";;
diff --git a/dev/include_printers b/dev/include_printers
new file mode 100644
index 0000000000..90088e40bf
--- /dev/null
+++ b/dev/include_printers
@@ -0,0 +1,55 @@
+#install_printer  (* pp_stdcmds *) pp;;
+#install_printer  (* pattern *) pppattern;;
+#install_printer  (* glob_constr *) ppglob_constr;;
+#install_printer  (* open constr *) ppopenconstr;;
+#install_printer  (* constr *) ppconstr;;
+#install_printer  (* econstr *) ppeconstr;;
+#install_printer  (* constr_substituted *) ppsconstr;;
+#install_printer  (* constraints *)  ppconstraints;;
+#install_printer  (* univ constraints *)  ppuniverseconstraints;;
+#install_printer  (* universe *)  ppuni;;
+#install_printer  (* universes *)  ppuniverses;;
+#install_printer  (* univ level *) ppuni_level;;
+#install_printer  (* univ context *) ppuniverse_context;;
+#install_printer  (* univ context future *) ppuniverse_context_future;;
+#install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* univ set *) ppuniverse_set;;
+#install_printer  (* univ instance *) ppuniverse_instance;;
+#install_printer  (* univ subst *) ppuniverse_subst;;
+#install_printer  (* univ full subst *) ppuniverse_level_subst;;
+#install_printer  (* univ opt subst *) ppuniverse_opt_subst;;
+#install_printer  (* evar univ ctx *) ppevar_universe_context;;
+#install_printer  (* inductive *) ppind;;
+#install_printer  (* 'a scheme_kind *) ppscheme;;
+#install_printer  (* type_judgement *) pptype;;
+#install_printer  (* judgement *) ppj;;
+#install_printer  (* id set *) ppidset;;
+#install_printer  (* int set *) ppintset;;
+
+#install_printer  (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
+#install_printer  (* Reductionops machine stack *) pp_stack_t;;
+
+(*#install_printer  (* hint_db *)  print_hint_db;;*)
+(*#install_printer  (* hints_path *)  pphintspath;;*)
+#install_printer  (* goal *)  ppgoal;;
+(*#install_printer  (* sigma goal *)  ppsigmagoal;;*)
+#install_printer  (* proof *)  pproof;;
+#install_printer  (* Goal.goal *)  ppgoalgoal;;
+#install_printer  (* proofview *)  ppproofview;;
+#install_printer  (* metaset.t *) ppmetas;;
+#install_printer  (* evar *)  ppevar;;
+#install_printer  (* evar_map *)  ppevm;;
+#install_printer  (* Evar.Set.t *) ppexistentialset;;
+#install_printer  (* clenv *) ppclenv;;
+#install_printer  (* env *) ppenv;;
+#install_printer  (* Hint_db.t *) pphintdb;;
+#install_printer  (* named_context_val *) ppnamedcontextval;;
+
+#install_printer  (* tactic *) pptac;;
+#install_printer  (* object *) ppobj;;
+#install_printer  (* global_reference *) ppglobal;;
+#install_printer  (* generic_argument *) pp_generic_argument;;
+
+#install_printer  (* fconstr *) ppfconstr;;
+
+#install_printer (* Future.computation *) ppfuture;;