From ce2efc0e02c4d164d9206361c0a2de6123816d00 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 5 Jan 2015 16:12:47 +0100 Subject: Updating documentation about bullets. Error messages were outdated. --- doc/refman/RefMan-pro.tex | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 4084424e81..018085e07b 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -353,15 +353,19 @@ with this priority ordering to have a correct indentation: {\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: 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. + 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: seems not finished.} + You are trying to use a bullet already in use but at a wrong level, + try instead. \end{ErrMsgs} -- cgit v1.2.3