diff options
| author | Paul Steckler | 2016-12-05 17:55:15 -0500 |
|---|---|---|
| committer | Paul Steckler | 2016-12-05 17:55:15 -0500 |
| commit | 2125949733b631426e955e722d6ca4e1b2eb5b60 (patch) | |
| tree | 655ab06b2fe50d0070c64a45ea16b2587f1a33a2 | |
| parent | 08c6e4c3dbe2ae851ef3097cc44618ea82717974 (diff) | |
Change module for Coq loop
| -rw-r--r-- | doc/refman/RefMan-com.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 784c9ccbbf..bef0a1686f 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 |