diff options
| author | Maxime Dénès | 2017-08-01 13:00:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-01 13:00:53 +0200 |
| commit | 82df5a27656753f50b5f5ff7d1faa37b2ddefc49 (patch) | |
| tree | 50698225f72a6e7cc09838ad245b7effde5d735c /doc | |
| parent | 2f349829c125ed0e2d55548935e7b90e7719f12e (diff) | |
| parent | 624dc13d0e80dcde22beecd3c80e68037899c287 (diff) | |
Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.
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}). |