diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2016-12-05 17:26:55 -0500 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2016-12-05 17:26:55 -0500 |
| commit | 08c6e4c3dbe2ae851ef3097cc44618ea82717974 (patch) | |
| tree | fb5add368017e958a541a5a918725b4f89e8bb53 /doc | |
| parent | 7aa2c39387a9781bf406c763c538859f24b8b7f3 (diff) | |
the -byte option is deprecated
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index c1e552a5d..784c9ccbb 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -26,8 +26,8 @@ run by the command {\tt coqtop}. They are two different binary images of \Coq: the byte-code one and the native-code one (if {\ocaml} provides a native-code compiler for your platform, which is supposed in the following). By default, -\verb!coqc! executes the native-code version; this can be overridden -using the \verb!-byte! option. +\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to +get the byte-code version. The byte-code toplevel is based on an {\ocaml} toplevel (to allow the dynamic link of tactics). You can switch to |