aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-06-14 18:58:03 +0200
committerEmilio Jesus Gallego Arias2017-07-27 12:36:13 +0200
commit624dc13d0e80dcde22beecd3c80e68037899c287 (patch)
treecf614a1ac45fbf1a5800e242434135d944e2a84c /doc
parent2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (diff)
[toplevel] Remove long ago deprecated and NOOP options.
Minor clean up, no sense in having these as they do nothing.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-oth.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3daaac88b1..bf48057cdf 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -656,7 +656,7 @@ dynamically.
searched into the current {\ocaml} loadpath (see the command {\tt
Add ML Path} in the Section~\ref{loadpath}). Loading of {\ocaml}
files is only possible under the bytecode version of {\tt coqtop}
-(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter
+(i.e. {\tt coqtop.byte}, see chapter
\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of
{\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
@@ -739,7 +739,7 @@ the command {\tt Declare ML Module} in the Section~\ref{compiled}).
\subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
This command displays the current {\ocaml} loadpath.
This command makes sense only under the bytecode version of {\tt
-coqtop}, i.e. using option {\tt -byte} (see the
+coqtop}, i.e. {\tt coqtop.byte} (see the
command {\tt Declare ML Module} in the section
\ref{compiled}).