diff options
| author | herbelin | 2012-08-07 22:49:04 +0000 |
|---|---|---|
| committer | herbelin | 2012-08-07 22:49:04 +0000 |
| commit | abe2f0cd9e529fb25c85cb9c93c8c4c09e28ee02 (patch) | |
| tree | c622efb06f9ee19b4c30466bf2ee748b9983e6b7 | |
| parent | df25e3e37addb8a5c9b41e251bc1ad3d6c9a4673 (diff) | |
Typo in r15654
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index eeeb983df0..d69098d0b5 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -259,7 +259,7 @@ there is no focused goal left). Unfocusing is then handled by {\tt \}} Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with 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 +of $g$ is completed, then it is mandatory to focus the next 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. |