diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-11 20:54:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-11 20:54:51 +0100 |
| commit | c2bb8e80ad013ae9021937b95ab01f92450341c5 (patch) | |
| tree | ea46795c3e4194b2eaaaa64bb252991c807d7fb1 /doc/refman/RefMan-tac.tex | |
| parent | b9585af9ef6e280ec1aa53e50833a3fa58c1763c (diff) | |
Documenting the tactic-in-term construction.
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 |