Added more informative messages about bullets.

Updated doc, but not tests-suite yet.

2 files changed, 20 insertions, 8 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index c5538aaab..0e820008e 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -205,6 +205,7 @@
 \newcommand{\pat}{\nterm{pat}}
 \newcommand{\pgs}{\nterm{pgms}}
 \newcommand{\pg}{\nterm{pgm}}
+\newcommand{\abullet}{\nterm{bullet}}
 %BEGIN LATEX
 \newcommand{\proof}{\nterm{proof}}
 %END LATEX
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 018085e07..25dc32e3d 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -353,19 +353,30 @@ with this priority ordering to have a correct indentation: {\tt -},
 the inner one, like in the example above.
 
 \begin{ErrMsgs}
+\item \errindex{Error: Wrong bullet: The current bullet {\abullet}
+  seems not finished.} You are trying to use a bullet already in use
+  but the current bullet {\abullet} is not finished.
+
+\item \errindex{Error: Wrong bullet: Finish bullet {\abullet}1 before
+  going back to {\abullet}2.} You need a bullet here but {\abullet}2,
+  despite already in use, is the wrong one. Use bullet {\abullet}1
+  instead.
+
+\item \errindex{Error: No focussed goal. To focus next goal, use
+  bullet {\abullet}.} You need a bullet here but you are trying to
+  introduce a fresh one. Use {\abullet} instead.
+
+\item \errindex{Error: Wrong bullet: no more goals at this level. Try
+  {\abullet} instead.} You need a bullet here but the one you just
+  tried is exhausted. Use {\abullet} instead.
+
 \item \errindex{Error: No such goal} there is no proof under focus
   (because it has just been solved), so the command you are trying
   to use cannot be applied. You need to first focus the next proof
   by using the bullet corresponding to the right level (using an
   incorrect bullet can also generates this message in some cases).
-\item \errindex{Error: No such goal (1)} Coq is expecting a given
-  bullet and you are trying to introduce a fresh one.
-\item \errindex{Error: This proof is focused, but cannot be unfocused
-  this way} You are trying to use a bullet that is already in use or a
-  {\tt \}} but the current subproof has not been fully solved.
-\item \errindex{Error: Wrong bullet: <bullet> seems not finished.}
-  You are trying to use a bullet already in use but at a wrong level,
-  try <bullet> instead.
+
+
 \end{ErrMsgs}