diff options
| author | Emilio Jesus Gallego Arias | 2017-06-14 18:58:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-07-27 12:36:13 +0200 |
| commit | 624dc13d0e80dcde22beecd3c80e68037899c287 (patch) | |
| tree | cf614a1ac45fbf1a5800e242434135d944e2a84c /doc | |
| parent | 2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (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.tex | 4 |
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}). |
