diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-04 10:59:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-04 10:59:35 +0100 |
| commit | 6131f89f6b91c45e641dd877df8719fa77987453 (patch) | |
| tree | 25d1189049e9f2d87cdba937db34b936d5450124 | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Fix typos.
| -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 6b24fdde7..0113c8df3 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} |