documentation of bullets (forward port from v8.4).

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

1 files changed, 40 insertions, 10 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index ca3a9cc985..eeeb983df0 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -248,15 +248,26 @@ only be unfocused when it has been fully solved (\emph{i.e.} when
 there is no focused goal left). Unfocusing is then handled by {\tt \}}
 (again, without a terminating period). See also example in next section.
 
+\begin{ErrMsgs}
+\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.
+\end{ErrMsgs}
+
 \subsection[Bullets]{Bullets\comindex{+ (command)}\comindex{- (command)}\comindex{* (command)}\index{Bullets}}
 Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with
-bullets. The use of a bullet for the first time focuses on the first
-goal, the same bullet cannot be used again until the subproof in
-completed, then it focuses on the next goal. Different bullets can be
-used to nest levels. The scope of bullet does not go beyond enclosing
-{\tt \{} and {\tt \}}, so bullets can be reused as further nesting
-level provided they are delimited by these. Available bullets are
-{\tt -}, {\tt +} and {\tt *} (without a terminating period).
+bullets. The use of a bullet $b$ for the first time focuses on the
+first goal $g$, the same bullet cannot be used again until the proof
+of $g$ is completed, then it is mandatory to focus  the bext goal with $b$. The
+consequence is that $g$ and all goals present when $g$ was focused are
+focused with the same bullet $b$. See the example below.
+
+Different bullets can be used to nest levels. The scope of bullet does
+not go beyond enclosing {\tt \{} and {\tt \}}, so bullets can be
+reused as further nesting levels provided they are delimited by these.
+Available bullets are {\tt -}, {\tt +} and {\tt *} (without a
+terminating period).
 
 The following example script illustrates all these features:
 \begin{coq_example*}
@@ -266,14 +277,33 @@ Proof.
   - split.
     + split.
       * { split.
-         - trivial.
-         - trivial.
+          - trivial.
+          - trivial.
         }
       * trivial.
     + trivial.
-  - trivial.
+  - assert True.
+    { trivial. }
+    assumption.
 \end{coq_example*}
 
+Remark: In ProofGeneral (emacs interface to coq), you must use bullets
+with this priority ordering to have a correct indentation: {\tt -},
+{\tt +}, {\tt *}. That is {\tt -} must be the outer bullet and {\tt *}
+the inner one, like in the example above.
+
+\begin{ErrMsgs}
+\item \errindex{Error: No such unproven subgoal} 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 also generates this message).
+\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.
+\end{ErrMsgs}
+
 
 \section{Requesting information}