From ab2ce06bffb0f06be96af24c0be546f5ebd11471 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Jan 2020 20:07:41 +0100
Subject: [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.
---
 doc/sphinx/practical-tools/coq-commands.rst | 2 --
 1 file changed, 2 deletions(-)

(limited to 'doc/sphinx')

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
-- 
cgit v1.2.3