Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.

45 files changed, 161 insertions, 582 deletions

diff --git a/.gitignore b/.gitignore
index 36536ec96..cec51986d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml
 
 kernel/byterun/coq_jumptbl.h
 kernel/copcodes.ml
-tools/tolink.ml
 ide/index_urls.txt
 .lia.cache
 checker/names.ml
diff --git a/Makefile b/Makefile
index 620fec546..2637996ed 100644
--- a/Makefile
+++ b/Makefile
@@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
@@ -246,7 +246,7 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN)
+	rm -f $(COQTOPEXE) $(CHICKEN)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
diff --git a/Makefile.build b/Makefile.build
index d548a8bd8..940943c41 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -228,8 +228,8 @@ endef
 
 define bestocaml
 $(if $(OPT),\
-$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\
-$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
+$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ && $(STRIP) $@ && $(CODESIGN) $@,\
+$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^)
 endef
 
 # Camlp5 settings
@@ -239,9 +239,8 @@ CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 
 PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
 
-SYSMOD:=str unix dynlink threads
-SYSCMA:=$(addsuffix .cma,$(SYSMOD))
-SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
+# Main packages linked by Coq.
+SYSMOD:=-package num,str,unix,dynlink,threads
 
 # We do not repeat the dependencies already in SYSMOD here
 P4CMA:=gramlib.cma
@@ -370,19 +369,30 @@ grammar/%.cmi: grammar/%.mli
 
 
 ###########################################################################
-# Main targets (coqmktop, coqtop.opt, coqtop.byte)
+# Main targets (coqtop.opt, coqtop.byte)
 ###########################################################################
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
 
 coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
+COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx
+COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo
+
+$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $<
+
 ifeq ($(BEST),opt)
-$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
+$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \
+	                   -I kernel/byterun/ -cclib -lcoqrun \
+                           $(SYSMOD) -package camlp5.gramlib \
+	                   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \
+	                   $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
 else
@@ -390,23 +400,14 @@ $(COQTOPEXE): $(COQTOPBYTE)
 	cp $< $@
 endif
 
-$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
+# Are "-cclib lcoqrun -dllib -lcoqrun" necessary?
+$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
-
-# coqmktop
-
-COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo
-
-$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO))
-	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
-
-tools/tolink.ml: Makefile.build Makefile.common
-	$(SHOW)"ECHO... >" $@
-	$(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
-	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
-	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
+	$(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \
+	                 -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \
+                         $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
+	                 $(LINKCMO) $(BYTEFLAGS) \
+	                 $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@
 
 # coqc
 
@@ -414,7 +415,7 @@ COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
 
 $(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
+	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 ###########################################################################
 # other tools
@@ -451,11 +452,11 @@ tools/coqdep_boot.cmx : tools/coqdep_common.cmx
 
 $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I tools, unix)
+	$(HIDE)$(call bestocaml, -I tools -package unix)
 
 $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I tools, unix)
+	$(HIDE)$(call bestocaml, -I tools -package unix)
 
 # The full coqdep (unused by this build, but distributed by make install)
 
@@ -466,36 +467,36 @@ COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \
 
 $(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
+	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,)
+	$(HIDE)$(call bestocaml,)
 
 COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,str unix threads)
+	$(HIDE)$(call bestocaml, -package str,unix,threads)
 
 $(COQTEX): $(call bestobj, tools/coq_tex.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,str)
+	$(HIDE)$(call bestocaml, -package str)
 
 $(COQWC): $(call bestobj, tools/coqwc.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,)
+	$(HIDE)$(call bestocaml, -package str)
 
 COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
 $(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,str unix)
+	$(HIDE)$(call bestocaml, -package str,unix)
 
 $(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,, $(SYSMOD))
+	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
@@ -506,13 +507,13 @@ FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo	ide/document.cmo \
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,-I ide,str unix threads)
+	$(HIDE)$(call bestocaml, -I ide -package str,unix,threads)
 
 # votour: a small vo explorer (based on the checker)
 
 bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I checker,)
+	$(HIDE)$(call bestocaml, -I checker)
 
 ###########################################################################
 # Csdp to micromega special targets
@@ -524,7 +525,7 @@ CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \
 
 $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,nums unix)
+	$(HIDE)$(call bestocaml, -package num,unix)
 
 ###########################################################################
 # tests
diff --git a/Makefile.checker b/Makefile.checker
index 435d8e8f6..b14f705be 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -29,7 +29,7 @@ CHKLIBS:= -I config -I lib -I checker
 ifeq ($(BEST),opt)
 $(CHICKEN): checker/check.cmxa checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
+	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP) $@
 	$(CODESIGN) $@
 else
@@ -39,7 +39,7 @@ endif
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
+	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
 
 checker/check.cma: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLC -a -o $@'
diff --git a/Makefile.common b/Makefile.common
index 4d63b08e2..f436d3e8f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -12,8 +12,6 @@
 # Executables
 ###########################################################################
 
-COQMKTOP:=bin/coqmktop$(EXE)
-
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
 
diff --git a/Makefile.install b/Makefile.install
index 27694106f..84aa11a5e 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -105,7 +105,6 @@ INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% configure.cmx, $(
 
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
@@ -140,7 +139,7 @@ install-coq-info: install-coq-manpages install-emacs install-latex
 MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
 	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
-	man/coq_makefile.1 man/coqmktop.1 man/coqchk.1
+	man/coq_makefile.1 man/coqchk.1
 
 install-coq-manpages:
 	$(MKDIR) $(FULLMANDIR)/man1
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 1271a02b0..22353ec16 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
   done
 
 (*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 6a834a304..40661f428 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -41,12 +41,8 @@ val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
-val osdeplibs : string  (* OS dependent link options for ocamlc *)
 val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
-
-(* val defined : string list  (* options for lib/ocamlpp *) *)
-
 val version : string    (* version number of Coq *)
 val caml_version : string    (* OCaml version used to compile Coq *)
 val caml_version_nums : int list    (* OCaml version used to compile Coq by components *)
diff --git a/configure.ml b/configure.ml
index 3850f119b..2292913d5 100644
--- a/configure.ml
+++ b/configure.ml
@@ -16,7 +16,7 @@ let coq_macos_version = "8.7.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8791
 let state_magic = 58791
-let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
+let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
@@ -680,17 +680,15 @@ let natdynlinkflag =
 
 (** * OS dependent libraries *)
 
-let osdeplibs = "-cclib -lunix"
-
-let operating_system, osdeplibs =
+let operating_system =
   if starts_with arch "sun4" then
     let os, _ = run "uname" ["-r"] in
     if starts_with os "5" then
-      "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket"
+      "Sun Solaris "^os
     else
-      "Sun OS "^os, osdeplibs
+      "Sun OS "^os
   else
-    (try Sys.getenv "OS" with Not_found -> ""), osdeplibs
+    (try Sys.getenv "OS" with Not_found -> "")
 
 (** Num library *)
 
@@ -1016,7 +1014,6 @@ let print_summary () =
     pr "  Operating system            : %s\n" operating_system;
   pr "  Coq VM bytecode link flags  : %s\n" (String.concat " " vmbyteflags);
   pr "  Other bytecode link flags   : %s\n" custom_flag;
-  pr "  OS dependent libraries      : %s\n" osdeplibs;
   pr "  OCaml version               : %s\n" caml_version;
   pr "  OCaml binaries in           : %s\n" (esc camlbin);
   pr "  OCaml library in            : %s\n" (esc camllib);
@@ -1109,7 +1106,6 @@ let write_configml f =
   pr_s "cflags" cflags;
   pr_s "caml_flags" caml_flags;
   pr_s "best" best_compiler;
-  pr_s "osdeplibs" osdeplibs;
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
   pr_li "caml_version_nums" caml_version_nums;
@@ -1240,7 +1236,6 @@ let write_makefile f =
   pr "# Supplementary libs for some systems, currently:\n";
   pr "#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n";
   pr "#  . others     : -cclib -lunix\n";
-  pr "OSDEPLIBS=%s\n\n" osdeplibs;
   pr "# executable files extension, currently:\n";
   pr "#  Unix systems:\n";
   pr "#  Win32 systems : .exe\n";
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index a6d8e4462..7e80e33c6 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -418,7 +418,6 @@ Binary file ./bin/coqchk.exe matches
 Binary file ./bin/coqdep.exe matches
 Binary file ./bin/coqdoc.exe matches
 Binary file ./bin/coqide.exe matches
-Binary file ./bin/coqmktop.exe matches
 Binary file ./bin/coqtop.byte.exe matches
 Binary file ./bin/coqtop.exe matches
 Binary file ./bin/coqworkmgr.exe matches
@@ -438,7 +437,6 @@ Binary file ./bin/ocamldoc.exe matches
 Binary file ./bin/ocamldoc.opt.exe matches
 Binary file ./bin/ocamlfind.exe matches
 Binary file ./bin/ocamlmklib.exe matches
-Binary file ./bin/ocamlmktop.exe matches
 Binary file ./bin/ocamlobjinfo.exe matches
 Binary file ./bin/ocamlopt.exe matches
 Binary file ./bin/ocamlopt.opt.exe matches
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index 7d3d811cc..fa145d498 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -73,8 +73,8 @@ Per function profiling
    To profile function foo in file bar.ml, add the following lines, just
    after the definition of the function:
 
-     let fookey = Profile.declare_profile "foo";;
-     let foo a b c = Profile.profile3 fookey foo a b c;;
+     let fookey = CProfile.declare_profile "foo";;
+     let foo a b c = CProfile.profile3 fookey foo a b c;;
 
    where foo is assumed to have three arguments (adapt using
    Profile.profile1, Profile. profile2, etc).
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 0c6d3ee80..26f3d0ddc 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and
 Some of the functions were you might want to set a breakpoint and see what happens next
 ---------------------------------------------------------------------------------------
 
-- Coqtop.start : This function is called by the code produced by "coqmktop".
+- Coqtop.start : This function is the main entry point of coqtop.
 - Coqtop.parse_args : This function is responsible for parsing command-line arguments.
 - Coqloop.loop : This function implements the read-eval-print loop.
 - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c411db100..962aa98b6 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -4,53 +4,24 @@
 The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
 
-\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}}
+\section[Using Coq as a library]{Using Coq as a library}
 
-The native-code version of \Coq\ cannot dynamically load user tactics
-using {\ocaml} code. It is possible to build a toplevel of \Coq,
-with {\ocaml} code statically linked, with the tool {\tt
-  coqmktop}.
-
-For example, one can build a native-code \Coq\ toplevel extended with a tactic
-which source is in {\tt tactic.ml} with the command
-\begin{verbatim}
-     % coqmktop -opt -o mytop.out tactic.cmx
-\end{verbatim}
-where {\tt tactic.ml} has been compiled with the native-code
-compiler {\tt ocamlopt}. This command generates an executable
-called {\tt mytop.out}. To use this executable to compile your \Coq\
-files, use {\tt coqc -image mytop.out}.
-
-A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
-which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
-
-
-\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}}
-
-One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
-order to debug your tactics with the {\ocaml} debugger.
-You need to have configured and compiled \Coq\ for debugging
-(see the file \texttt{INSTALL} included in the distribution).
-Then, you must compile the Caml modules of your tactic with the
-option \texttt{-g} (with the bytecode compiler) and build a stand-alone
-bytecode toplevel with the following command:
+In previous versions, \texttt{coqmktop} was used to build custom
+toplevels --- for example for better debugging or custom static
+linking. Nowadays, the preferred method is to use \texttt{ocamlfind}.
 
+The most basic custom toplevel is built using:
 \begin{quotation}
-\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>}
+\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
+  -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
 
-
-To launch the \ocaml\ debugger with the image you need to execute it in
-an environment which correctly sets the \texttt{COQLIB} variable.
-Moreover, you have to indicate the directories in which
-\texttt{ocamldebug} should search for Caml modules.
-
-A possible solution is to use a wrapper around \texttt{ocamldebug}
-which detects the executables containing the word \texttt{coq}. In
-this case, the debugger is called with the required additional
-arguments. In other cases, the debugger is simply called without additional
-arguments. Such a wrapper can be found in the \texttt{dev/}
-subdirectory of the sources.
+For example, to statically link LTAC, you can just do:
+\begin{quotation}
+\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
+  -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+\end{quotation}
+and similarly for other plugins.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 6566ad989..6131f4c03 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -240,8 +240,8 @@ let add_constraints ctx cstrs =
       uctx_univ_variables = vars;
       uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
-(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
+(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
+(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
 
 let add_universe_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
diff --git a/engine/universes.ml b/engine/universes.ml
index 0250295fd..30490ec56 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -946,8 +946,8 @@ let normalize_context_set ctx us algs =
   let us = normalize_opt_subst us in
     (us, algs), (ctx', Constraint.union noneqs eqs)
 
-(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
+(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
 
 let is_trivial_leq (l,d,r) =
   Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2579ac045..7b921d35b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } =
     cook_context = Some const_hyps;
   }
 
-(* let cook_constant_key = Profile.declare_profile "cook_constant" *)
-(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *)
+(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
+(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
 
 let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 62aa9a2d7..2a629f00a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
     ()
 
 (*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0f4a1e5f..c07ac973b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
 let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) =
   let evars, univs = evars in
   if Flags.profile then
-    let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
-      Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
+    let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
+      CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
   else gen_conv cv_pb l2r reds env evars univs
 
 let conv = gen_conv CONV
@@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
 (* Profiling *)
 let infer_conv_universes = 
   if Flags.profile then 
-    let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in
-      Profile.profile8 infer_conv_universes_key infer_conv_universes
+    let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
+      CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
 let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
@@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 =
 
 let default_conv_leq = default_conv CUMUL
 (*
-let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
+let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
-  Profile.profile4 convleqkey conv_leq env t1 t2;;
+  CProfile.profile4 convleqkey conv_leq env t1 t2;;
 
-let convkey = Profile.declare_profile "Kernel_reduction.conv";;
+let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
 let conv env t1 t2 =
-  Profile.profile4 convleqkey conv env t1 t2;;
+  CProfile.profile4 convleqkey conv env t1 t2;;
 *)
 
 (* Application with on-the-fly reduction *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4ccef5c38..4a935f581 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -435,8 +435,8 @@ let infer env constr =
 
 let infer = 
   if Flags.profile then
-    let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile2 infer_key (fun b c -> infer b c)
+    let infer_key = CProfile.declare_profile "Fast_infer" in
+      CProfile.profile2 infer_key (fun b c -> infer b c)
   else (fun b c -> infer b c)
 
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 00c0ea70d..f1e8d1031 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -890,24 +890,24 @@ let dump_universes output g =
 
 let merge_constraints = 
   if Flags.profile then 
-    let key = Profile.declare_profile "merge_constraints" in
-      Profile.profile2 key merge_constraints
+    let key = CProfile.declare_profile "merge_constraints" in
+      CProfile.profile2 key merge_constraints
   else merge_constraints
 let check_constraints =
   if Flags.profile then
-    let key = Profile.declare_profile "check_constraints" in
-      Profile.profile2 key check_constraints
+    let key = CProfile.declare_profile "check_constraints" in
+      CProfile.profile2 key check_constraints
   else check_constraints
 
 let check_eq = 
   if Flags.profile then
-    let check_eq_key = Profile.declare_profile "check_eq" in
-      Profile.profile3 check_eq_key check_eq
+    let check_eq_key = CProfile.declare_profile "check_eq" in
+      CProfile.profile3 check_eq_key check_eq
   else check_eq
 
 let check_leq = 
   if Flags.profile then 
-    let check_leq_key = Profile.declare_profile "check_leq" in
-      Profile.profile3 check_leq_key check_leq
+    let check_leq_key = CProfile.declare_profile "check_leq" in
+      CProfile.profile3 check_leq_key check_leq
   else check_leq
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f52d734ef..eae917b5a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -133,8 +133,8 @@ let substn_many lamv n c =
     substrec n c
 
 (*
-let substkey = Profile.declare_profile "substn_many";;
-let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
+let substkey = CProfile.declare_profile "substn_many";;
+let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;;
 *)
 
 let make_subst = function
@@ -274,8 +274,8 @@ let subst_univs_constr subst c =
 
 let subst_univs_constr = 
   if Flags.profile then
-    let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in
-      Profile.profile2 subst_univs_constr_key subst_univs_constr
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
   else subst_univs_constr
 
 let subst_univs_level_constr subst c =
@@ -347,8 +347,8 @@ let subst_instance_constr subst c =
     in
     aux c
 
-(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
+(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
+(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
diff --git a/lib/profile.ml b/lib/cProfile.ml
index 0bc226a45..0bc226a45 100644
--- a/lib/profile.ml
+++ b/lib/cProfile.ml
diff --git a/lib/profile.mli b/lib/cProfile.mli
index cae4397a1..cae4397a1 100644
--- a/lib/profile.mli
+++ b/lib/cProfile.mli
diff --git a/lib/envars.ml b/lib/envars.ml
index 206d75033..8ebf84057 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -153,19 +153,17 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let ocamlfind () =
-  if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
+let ocamlfind () = Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
 let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
 
 let camlp4bin () =
-  if !Flags.camlp4bin_spec then !Flags.camlp4bin else
-    if !Flags.boot then Coq_config.camlp4bin else
-      try guess_camlp4bin ()
-      with Not_found ->
-        Coq_config.camlp4bin
+  if !Flags.boot then Coq_config.camlp4bin else
+    try guess_camlp4bin ()
+    with Not_found ->
+      Coq_config.camlp4bin
 
 let camlp4 () = camlp4bin () / exe Coq_config.camlp4
 
diff --git a/lib/flags.ml b/lib/flags.ml
index b43d5f74d..9631da633 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -153,14 +153,6 @@ let is_standard_doc_url url =
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
 
-(* Options for changing ocamlfind (used by coqmktop) *)
-let ocamlfind_spec = ref false
-let ocamlfind = ref Coq_config.camlbin
-
-(* Options for changing camlp4bin (used by coqmktop) *)
-let camlp4bin_spec = ref false
-let camlp4bin = ref Coq_config.camlp4bin
-
 (* Level of inlining during a functor application *)
 
 let default_inline_level = 100
diff --git a/lib/flags.mli b/lib/flags.mli
index b82fe6128..1b1e264f0 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -122,12 +122,6 @@ val is_standard_doc_url : string -> bool
 val coqlib_spec : bool ref
 val coqlib : string ref
 
-(** Options for specifying where OCaml binaries reside *)
-val ocamlfind_spec : bool ref
-val ocamlfind : string ref
-val camlp4bin_spec : bool ref
-val camlp4bin : string ref
-
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 8791f0741..66f939a91 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -9,7 +9,7 @@ System
 CThread
 Spawn
 Trie
-Profile
+CProfile
 Explore
 Predicate
 Rtree
diff --git a/man/coqmktop.1 b/man/coqmktop.1
deleted file mode 100644
index 810df782c..000000000
--- a/man/coqmktop.1
+++ /dev/null
@@ -1,71 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coqmktop \- The Coq Proof Assistant user-tactics linker
-
-
-.SH SYNOPSIS
-.B coqmktop
-[
-.I options
-]
-.I files
-
-
-.SH DESCRIPTION
-
-.B coqmktop
-builds a new Coq toplevel extended with user-tactics.
-.IR files \&
-are the Objective Caml object or library files
-(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system.
-The linker produces an executable Coq toplevel which can be called
-directly or through coqc(1), using the \-image option.
-
-.SH OPTIONS
-
-.TP
-.BI \-h
-Help. List the available options.
-
-.TP
-.BI \-srcdir \ dir
-Specify where the Coq source files are
-
-.TP
-.BI \-o \ exec\-file
-Specify the name of the resulting toplevel
-
-.TP
-.B \-opt
-Compile in native code
-
-.TP
-.B \-full
-Link high level tactics
-
-.TP
-.B \-top
-Build Coq on a ocaml toplevel (incompatible with
-.BR \-opt )
-
-.TP
-.BI \-R \ dir
-Specify recursively directories for Ocaml
-
-.TP
-.B \-v8
-Link with V8 grammar
-
-
-.SH SEE ALSO
-
-.BR coqtop (1),
-.BR ocamlmktop (1).
-.BR ocamlc (1).
-.BR ocamlopt (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1f2e5f7ac..2e14243d8 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -361,8 +361,8 @@ end) = struct
 end
 
 (* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* let mytypeofkey = Profile.declare_profile "my_type_of";; *)
-(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *)
+(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
+(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)
 
 
 let type_app_poly env env evd f args =
@@ -2086,8 +2086,8 @@ let get_hyp gl (c,l) clause l2r =
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
-(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *)
-(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
+(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *)
+(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
 
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5776d2ec..cb8844623 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true)
 (* Profiling *)
 let evar_conv_x =
   if Flags.profile then
-    let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
-      Profile.profile6 evar_conv_xkey evar_conv_x
+    let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in
+      CProfile.profile6 evar_conv_xkey evar_conv_x
   else evar_conv_x
 
 let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 318176611..d9994c473 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1269,11 +1269,11 @@ let nf_all env sigma =
 (*                         Conversion                               *)
 (********************************************************************)
 (*
-let fkey = Profile.declare_profile "fhnf";;
-let fhnf info v = Profile.profile2 fkey fhnf info v;;
+let fkey = CProfile.declare_profile "fhnf";;
+let fhnf info v = CProfile.profile2 fkey fhnf info v;;
 
-let fakey = Profile.declare_profile "fhnf_apply";;
-let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
+let fakey = CProfile.declare_profile "fhnf_apply";;
+let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;;
 *)
 
 let is_transparent e k =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f8f086fad..00b175c48 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 (*   let f,_,_,_ = retype ~polyprop sigma in *)
 (*     if lax then f env c else anomaly_on_error (f env) c  *)
 
-(* let get_type_of_key = Profile.declare_profile "get_type_of" *)
-(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *)
+(* let get_type_of_key = CProfile.declare_profile "get_type_of" *)
+(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *)
 
 (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *)
 (*   get_type_of polyprop lax env sigma c *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 85383ba39..5a522e06a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
 
 let whd_simpl_stack = 
   if Flags.profile then 
-    let key = Profile.declare_profile "whd_simpl_stack" in
-      Profile.profile3 key whd_simpl_stack
+    let key = CProfile.declare_profile "whd_simpl_stack" in
+      CProfile.profile3 key whd_simpl_stack
   else whd_simpl_stack
 
 (* Same as [whd_simpl] but also reduces constants that do not hide a
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2e213a51d..b49da57a4 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail =
   Hook.get get_solve_all_instances env evd filter unique split fail
 
 (** Profiling resolution of typeclasses *)
-(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
-(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
+(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
+(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
 
 let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 84ffab426..08329391d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 =
 
 let w_unify = 
   if Flags.profile then
-    let wunifkey = Profile.declare_profile "w_unify" in
-      Profile.profile6 wunifkey w_unify
+    let wunifkey = CProfile.declare_profile "w_unify" in
+      CProfile.profile6 wunifkey w_unify
   else w_unify
 
 let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3e3313eb5..cd2b10906 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -30,8 +30,8 @@ let refiner pr goal_sigma =
 (* Profiling refiner *)
 let refiner = 
   if Flags.profile then
-    let refiner_key = Profile.declare_profile "refiner" in
-      Profile.profile2 refiner_key refiner
+    let refiner_key = CProfile.declare_profile "refiner" in
+      CProfile.profile2 refiner_key refiner
   else refiner
 
 (*********************)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fa8435d1f..e7e21b5f4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames =
 
 let delta_auto = 
   if Flags.profile then
-    let key = Profile.declare_profile "delta_auto" in
-      Profile.profile5 key delta_auto
+    let key = CProfile.declare_profile "delta_auto" in
+      CProfile.profile5 key delta_auto
   else delta_auto
 
 let auto ?(debug=Off) n = delta_auto debug false n
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index d2e014e55..6ea6155e0 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -404,8 +404,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
     pr_info_nop d;
     user_err Pp.(str "eauto: search failed")
 
-(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
-(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
+(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *)
+(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
 
 let eauto_with_bases ?(debug=Off) np lems db_list =
   tclTRY (e_search_auto debug np lems db_list)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6aa052d32..839090903 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1982,11 +1982,11 @@ let cut_and_apply c =
 (*               Exact tactics                                      *)
 (********************************************************************)
 
-(* let convert_leqkey = Profile.declare_profile "convert_leq";; *)
-(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *)
+(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *)
+(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *)
 
-(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
-(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
+(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *)
+(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *)
 
 let exact_no_check c =
   Refine.refine ~typecheck:false (fun h -> (h,c))
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 80b1f584b..2b56c63a0 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -87,7 +87,6 @@ COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
 GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
-COQMKTOP ?= "$(COQBIN)coqmktop"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
 
 # Timing scripts
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
deleted file mode 100644
index 950ed53cc..000000000
--- a/tools/coqmktop.ml
+++ /dev/null
@@ -1,314 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** {1 Coqmktop} *)
-
-(** coqmktop is a script to link Coq, analogous to ocamlmktop.
-   The command line contains options specific to coqmktop, options for the
-   Ocaml linker and files to link (in addition to the default Coq files). *)
-
-(** {6 Utilities} *)
-
-(** Split a string at each blank
-*)
-let split_list =
-  let spaces = Str.regexp "[ \t\n]+" in
-  fun str -> Str.split spaces str
-
-[@@@ocaml.warning "-3"]       (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-[@@@ocaml.warning "+3"]
-
-let (/) = Filename.concat
-
-(** Which user files do we support (and propagate to ocamlopt) ?
-*)
-let supported_suffix f = match CUnix.get_extension f with
-  | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
-  | _ -> false
-
-let supported_flambda_option f = List.mem f Coq_config.flambda_flags
-
-(** From bytecode extension to native
-*)
-let native_suffix f = match CUnix.get_extension f with
-  | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx"
-  | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa"
-  | ".a" -> f
-  | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a")
-
-(** Transforms a file name in the corresponding Caml module name.
-*)
-let module_of_file name =
-  capitalize (try Filename.chop_extension name with Invalid_argument _ -> name)
-
-(** Run a command [prog] with arguments [args].
-    We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
-*)
-let run_command prog args =
-  match CUnix.sys_command prog args with
-  | Unix.WEXITED 127 -> failwith ("no such command "^prog)
-  | Unix.WEXITED n -> n
-  | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n)
-  | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n)
-
-
-
-(** {6 Coqmktop options} *)
-
-let opt        = ref false
-let top        = ref false
-let echo       = ref false
-let no_start   = ref false
-
-let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
-
-(** {6 Includes options} *)
-
-(** Since the Coq core .cma are given with their relative paths
-    (e.g. "lib/clib.cma"), we only need to include directories mentionned in
-    the temp main ml file below (for accessing the corresponding .cmi). *)
-
-let std_includes basedir =
-  let rebase d = match basedir with None -> d | Some base -> base / d in
-  ["-I"; rebase ".";
-   "-I"; rebase "lib";
-   "-I"; rebase "vernac";       (* For Mltop *)
-   "-I"; rebase "toplevel";
-   "-I"; rebase "kernel/byterun";
-   "-I"; Envars.camlp4lib () ] @
-  (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
-
-(** For the -R option, visit all directories under [dir] and add
-    corresponding -I to the [opts] option list (in reversed order) *)
-let incl_all_subdirs dir opts =
-  let l = ref opts in
-  let add f = l := f :: "-I" :: !l in
-  let rec traverse dir =
-    if Sys.file_exists dir && Sys.is_directory dir then
-      let () = add dir in
-      let subdirs = try Sys.readdir dir with any -> [||] in
-      Array.iter (fun f -> traverse (dir/f)) subdirs
-  in
-  traverse dir; !l
-
-
-(** {6 Objects to link} *)
-
-(** NB: dynlink is now always linked, it is used for loading plugins
-    and compiled vm code (see native-compiler). We now reject platforms
-    with ocamlopt but no dynlink.cmxa during ./configure, and give
-    instructions there about how to build a dummy dynlink.cmxa,
-    cf. dev/dynlink.ml. *)
-
-(** OCaml + CamlpX libraries *)
-
-let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4_libs = ["gramlib.cma"]
-let libobjs = ocaml_libs @ camlp4_libs
-
-(** Toplevel objects *)
-
-let ocaml_topobjs =
-  if is_ocaml4 then
-    ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"]
-  else
-    ["toplevellib.cma"]
-
-let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
-
-let topobjs = ocaml_topobjs @ camlp4_topobjs
-
-(** Coq Core objects *)
-
-let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts)
-let core_objs = split_list Tolink.core_objs
-let core_libs = split_list Tolink.core_libs
-
-(** Build the list of files to link and the list of modules names
-*)
-let files_to_link userfiles =
-  let top = if !top then topobjs else [] in
-  let modules = List.map module_of_file (top @ core_objs @ userfiles) in
-  let objs = libobjs @ top @ core_libs in
-  let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles
-  in (modules, objs')
-
-
-(** {6 Parsing of the command-line} *)
-
-let usage () =
-  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
-\nFlags are:\
-\n  -coqlib dir    Specify where the Coq object files are\
-\n  -ocamlfind dir Specify where the ocamlfind binary is\
-\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
-\n  -o exec-file   Specify the name of the resulting toplevel\
-\n  -boot          Run in boot mode\
-\n  -echo          Print calls to external commands\
-\n  -opt           Compile in native code\
-\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
-\n  -R dir         Add recursively dir to OCaml search path\
-\n";
-  exit 1
-
-let parse_args () =
-  let rec parse (op,fl) = function
-    | [] -> List.rev op, List.rev fl
-
-    (* Directories *)
-    | "-coqlib" :: d :: rem ->
-	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
-    | "-ocamlfind" :: d :: rem ->
-	Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem
-    | "-camlp4bin" :: d :: rem ->
-	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
-    | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
-    | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage ()
-
-    (* Boolean options of coqmktop *)
-    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
-    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
-    | "-top" :: rem -> top := true ; parse (op,fl) rem
-    | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
-    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
-
-    (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
-    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
-        parse (o::op,fl) rem
-    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
-	begin
-	  match rem' with
-	    | a :: rem -> parse (a::o::op,fl) rem
-	    | []       -> usage ()
-	end
-
-    | ("-h"|"-help"|"--help") :: _ -> usage ()
-    | f :: rem when supported_flambda_option f -> parse (op,fl) rem
-    | f :: rem when supported_suffix f -> parse (op,f::fl) rem
-    | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
-  in
-  parse ([],[]) (List.tl (Array.to_list Sys.argv))
-
-
-(** {6 Temporary main file} *)
-
-(** remove the temporary main file
-*)
-let clean file =
-  let rm f = if Sys.file_exists f then Sys.remove f in
-  let basename = Filename.chop_suffix file ".ml" in
-  if not !echo then begin
-    rm file;
-    rm (basename ^ ".o");
-    rm (basename ^ ".cmi");
-    rm (basename ^ ".cmo");
-    rm (basename ^ ".cmx")
-  end
-
-(** Initializes the kind of loading in the main program
-*)
-let declare_loading_string () =
-  if not !top then
-    "Mltop.remove ();;"
-  else
-    "begin try\
-\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
-\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
-\n         | Toploop.Directive_none f -> f ()\
-\n         | _ -> ()\
-\n       end\
-\n     with\
-\n       | Not_found -> ()\
-\n     end;;\
-\n\
-\n     let ppf = Format.std_formatter;;\
-\n     Mltop.set_top\
-\n       {Mltop.load_obj=\
-\n         (fun f -> if not (Topdirs.load_file ppf f)\
-\n                   then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\
-\n        Mltop.use_file=Topdirs.dir_use ppf;\
-\n        Mltop.add_dir=Topdirs.dir_directory;\
-\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
-\n"
-
-(** create a temporary main file to link
-*)
-let create_tmp_main_file modules =
-  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
-  try
-    (* Add the pre-linked modules *)
-    output_string oc "List.iter Mltop.add_known_module [\"";
-    output_string oc (String.concat "\";\"" modules);
-    output_string oc "\"];;\n";
-    (* Initializes the kind of loading *)
-    output_string oc (declare_loading_string());
-    (* Start the toplevel loop *)
-    if not !no_start then output_string oc "Coqtop.start();;\n";
-    close_out oc;
-    main_name
-  with reraise ->
-    clean main_name; raise reraise
-
-(* TODO: remove once OCaml 4.04 is adopted *)
-let split_on_char sep s =
-  let r = ref [] in
-  let j = ref (String.length s) in
-  for i = String.length s - 1 downto 0 do
-      if s.[i] = sep then begin
-      r := String.sub s (i + 1) (!j - i - 1) :: !r;
-      j := i
-    end
-  done;
-  String.sub s 0 !j :: !r
-
-(** {6 Main } *)
-
-let main () =
-  let (options, userfiles) = parse_args () in
-  (* Directories: *)
-  let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in
-  let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
-  (* Which ocaml compiler to invoke *)
-  let prog = if !opt then "opt" else "ocamlc" in
-  (* Which arguments ? *)
-  if !opt && !top then failwith "no custom toplevel in native code!";
-  let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in
-  let topstart = if !top then [ "topstart.cmo" ] else [] in
-  let (modules, tolink) = files_to_link userfiles in
-  let main_file = create_tmp_main_file modules in
-  try
-    (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
-       - With the coq .cma, we MUST use the -linkall option. *)
-    let coq_camlflags =
-      List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in
-    let args =
-      coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @
-      (std_includes basedir) @ tolink @ [ main_file ] @ topstart
-    in
-    if !echo then begin
-      let command = String.concat " " (Envars.ocamlfind ()::prog::args) in
-      print_endline command;
-      print_endline
-	("(command length is " ^
-	    (string_of_int (String.length command)) ^ " characters)");
-      flush Pervasives.stdout
-    end;
-    let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in
-    clean main_file;
-    exitcode
-  with reraise -> clean main_file; raise reraise
-
-let pr_exn = function
-  | Failure msg -> msg
-  | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err
-  | any -> Printexc.to_string any
-
-let _ =
-  try exit (main ())
-  with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6048dae3b..2fa9f0ab4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -756,7 +756,7 @@ let init_toplevel arglist =
   (* Coq's init process, phase 1:
      - OCaml parameters, and basic structures and IO
    *)
-  Profile.init_profile ();
+  CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
@@ -846,7 +846,5 @@ let start () =
       let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
     end;
-    Profile.print_profile ();
+    CProfile.print_profile ();
     exit 0
-
-(* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml
new file mode 100644
index 000000000..56aced92a
--- /dev/null
+++ b/toplevel/coqtop_bin.ml
@@ -0,0 +1,2 @@
+(* Main coqtop initialization *)
+let () = Coqtop.start()
diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml
new file mode 100644
index 000000000..7d8354ec3
--- /dev/null
+++ b/toplevel/coqtop_byte_bin.ml
@@ -0,0 +1,21 @@
+let drop_setup () =
+  begin try
+    (* Enable rectypes in the toplevel if it has the directive #rectypes *)
+    begin match Hashtbl.find Toploop.directive_table "rectypes" with
+      | Toploop.Directive_none f -> f ()
+      | _ -> ()
+    end
+    with
+    | Not_found -> ()
+  end;
+  let ppf = Format.std_formatter in
+  Mltop.(set_top
+           { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
+                          then CErrors.user_err Pp.(str ("Could not load plugin "^f))
+                        );
+             use_file = Topdirs.dir_use ppf;
+             add_dir  = Topdirs.dir_directory;
+             ml_loop  = (fun () -> Toploop.loop ppf);
+           })
+
+let _ = drop_setup ()
diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml
new file mode 100644
index 000000000..410b4679a
--- /dev/null
+++ b/toplevel/coqtop_opt_bin.ml
@@ -0,0 +1,3 @@
+let drop_setup () = Mltop.remove ()
+
+let _ = drop_setup ()