[make] remove unneeded generated file "tolink.ml"

When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.

This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.

Fixes #6364.

1 files changed, 4 insertions, 7 deletions

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 002e9625c..962aa98b6 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -12,19 +12,16 @@ linking. Nowadays, the preferred method is to use \texttt{ocamlfind}.
 
 The most basic custom toplevel is built using:
 \begin{quotation}
-\texttt{\% make tools/tolink.cmx}
 \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
-  -package coq.toplevel -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+  -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
 
-For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use:
+For example, to statically link LTAC, you can just do:
 \begin{quotation}
-\texttt{\% make tools/tolink.cmx}
 \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
-  -package coq.toplevel -package coq.ltac -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+  -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
-
-We will remove the need for the \texttt{tolink} file in the future.
+and similarly for other plugins.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%