From 08c6e4c3dbe2ae851ef3097cc44618ea82717974 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 5 Dec 2016 17:26:55 -0500 Subject: the -byte option is deprecated --- doc/refman/RefMan-com.tex | 4 ++-- 1 file 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 -- cgit v1.2.3 From 2125949733b631426e955e722d6ca4e1b2eb5b60 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 5 Dec 2016 17:55:15 -0500 Subject: Change module for Coq loop --- doc/refman/RefMan-com.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 784c9ccbb..bef0a1686 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -32,7 +32,7 @@ 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 -- cgit v1.2.3