[rfc] [mltop] Removal of dynamic loading of object and `.ml` files

This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)

It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.

2 files changed, 5 insertions, 2 deletions

diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst
new file mode 100644
index 0000000000..db433ad64c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  The `-load-ml-source` and `-load-ml-object` command line options
+  have been removed; their use was very limited, you can achieve the same adding
+  additional object files in the linking step or using a plugin.
+  (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index ba43128bdc..98d222e317 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise:
   loading the default resource file from the standard configuration
   directories.
 :-q: Do not to load the default resource file.
-:-load-ml-source *file*: Load the OCaml source file *file*.
-:-load-ml-object *file*: Load the OCaml object file *file*.
 :-l *file*, -load-vernac-source *file*: Load and execute the |Coq|
   script from *file.v*.
 :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the