From 6131f89f6b91c45e641dd877df8719fa77987453 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 4 Mar 2018 10:59:35 +0100
Subject: Fix typos.

---
 doc/refman/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 6b24fdde79..0113c8df34 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -306,7 +306,7 @@ This command restores to focus the goal that were suspended by the
 last {\tt Focus} command.
 
 \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
-Succeeds in the proof is fully unfocused, fails is there are some
+Succeeds in the proof if fully unfocused, fails if there are some
 goals out of focus.
 
 \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
-- 
cgit v1.2.3