coqide menus on golas

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8403 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 3 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 223585d54c..87c8e3edb6 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -160,7 +160,8 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{Warnings}
-\item {\tt Warning: {\ident$_i$} cannot be defined.}\\
+\item {\tt Warning: {\ident$_i$} cannot be defined.}
+
   It can happen that the definition of a projection is impossible.
   This message is followed by an explanation of this impossibility.
   There may be three reasons:
@@ -170,7 +171,7 @@ Reset Initial.
    \item The body of {\ident$_i$} uses an incorrect elimination for
      {\ident} (see sections \ref{Fixpoint} and \ref{Caseexpr}).
    \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves couldn't be defined.\\
+   projections which themselves couldn't be defined.
    \end{enumerate}  
 \end{Warnings}     
 
@@ -830,7 +831,9 @@ contextual implicit arguments must be considered or not (see sections
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive list (A:Set) : Set := nil : list A | cons : A -> list A -> list A.
+Inductive list (A:Set) : Set := 
+  | nil : list A 
+  | cons : A -> list A -> list A.
 \end{coq_example*}
 \begin{coq_example}
 Implicit Arguments cons.