diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-06 09:15:53 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-12-06 09:15:53 +0100 |
| commit | 7febc54ba8a41d16809b052f86ff338c714bf9f0 (patch) | |
| tree | 655ab06b2fe50d0070c64a45ea16b2587f1a33a2 | |
| parent | 7aa2c39387a9781bf406c763c538859f24b8b7f3 (diff) | |
| parent | 2125949733b631426e955e722d6ca4e1b2eb5b60 (diff) | |
Merge remote-tracking branch 'github/pr/389' into v8.6
Was PR#389: Changed mention of deprecated -byte option to .byte suffix;
change module for Coq loop
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index c1e552a5d..bef0a1686 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -26,13 +26,13 @@ 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 the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the -\Coq~toplevel with the command \verb!Toplevel.loop();;!. +\Coq~toplevel with the command \verb!Coqloop.loop();;!. \section{Batch compilation ({\tt coqc})} The {\tt coqc} command takes a name {\em file} as argument. Then it |