From 79490d29774277801ccd4b7fa68dd9770bab8a6f Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 5 Jan 2004 08:30:35 +0000
Subject: correction bugs commit precedent et mise en forme html

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8456 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-com.tex | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'doc/RefMan-com.tex')

diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index da21ec4672..34e4211493 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -3,20 +3,17 @@
 \ttindex{coqc}
 
 There are two \Coq~commands: 
-
-\bigskip
-\begin{tabular}{l@{\quad:\quad}l}
-  -- {\tt coqtop} & The \Coq\ toplevel (interactive mode) ; \\[1em]
-  -- {\tt coqc}   & The \Coq\ compiler (batch compilation).
-\end{tabular}
-\bigskip
-
+\begin{itemize}
+\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
+\item {\tt coqc} : The \Coq\ compiler (batch compilation).
+\end{itemize}
 The options are (basically) the same for the two commands, and
 roughly described below. You can also look at the \verb!man! pages of
 \verb!coqtop! and \verb!coqc! for more details.
 
 
 \section{Interactive use ({\tt coqtop})}
+
 In the interactive mode, also known as the \Coq~toplevel, the user can
 develop his theories and proofs step by step.  The \Coq~toplevel is
 run by the command {\tt coqtop}. 
@@ -173,7 +170,7 @@ The following command-line options are recognized by the commands {\tt
   only available for {\tt coqtop}.
 
 %\item[{\tt -compile-verbose} {\em file}]\ 
-@
+
 %  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
 %  a copy of the contents of the file on standard input.
 %  This option implies options {\tt -batch} and {\tt -silent}. It is
-- 
cgit v1.2.3