aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2016-12-05 17:55:15 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2016-12-05 17:55:15 -0500
commit2125949733b631426e955e722d6ca4e1b2eb5b60 (patch)
tree655ab06b2fe50d0070c64a45ea16b2587f1a33a2 /doc
parent08c6e4c3dbe2ae851ef3097cc44618ea82717974 (diff)
Change module for Coq loop
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-com.tex2
1 files changed, 1 insertions, 1 deletions
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