diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 8 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6b24fdde79..bd74a40d7c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,15 +298,19 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. - \end{Variant} +\emph{This command is deprecated since 8.8: prefer the use of bullets or + focusing brackets instead, including {\tt {\num}: \{}}. + \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} This command restores to focus the goal that were suspended by the last {\tt Focus} command. +\emph{This command is deprecated since 8.8.} + \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} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a2739e457e..8c09b23a5a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -598,5 +598,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq86.v theories/Compat/Coq87.v + theories/Compat/Coq88.v </dd> </dl> |