From abe2f0cd9e529fb25c85cb9c93c8c4c09e28ee02 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 7 Aug 2012 22:49:04 +0000
Subject: Typo in r15654

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
 
-- 
cgit v1.2.3