Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes

1 files changed, 0 insertions, 16 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a38c26c2b3..d1f3dcc309 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged.
    :n:`-Q @string @dirpath`. It adds the physical directory string to the current
    |Coq| loadpath and maps it to the logical directory dirpath.
 
-   .. cmdv:: Add LoadPath @string
-
-      Performs as :n:`Add LoadPath @string @dirpath` but
-      for the empty directory path.
-
 
 .. cmd:: Add Rec LoadPath @string as @dirpath
 
@@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged.
    :n:`-R @string @dirpath`. It adds the physical directory string and all its
    subdirectories to the current |Coq| loadpath.
 
-   .. cmdv:: Add Rec LoadPath @string
-
-      Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty
-      logical directory path.
-
 
 .. cmd:: Remove LoadPath @string
 
@@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged.
    loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
-.. cmd:: Add Rec ML Path @string
-
-   This command adds the directory :n:`@string` and all its subdirectories to
-   the current OCaml loadpath (see the command :cmd:`Declare ML Module`).
-
-
 .. cmd:: Print ML Path @string
 
    This command displays the current OCaml loadpath. This