diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 399ea8f99..e318446a4 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3813,7 +3813,7 @@ e.g. \texttt{Require Import A.}). \end{Variants} -\subsubsection{\tt Declare Implicit Tactic {\tac}} +\subsubsection{\tt Declare Implicit Tactic {\tac}}\label{DeclareImplicit} \comindex{Declare Implicit Tactic} This command declares a tactic to be used to solve implicit arguments |