diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 14:22:25 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 14:22:25 +0100 |
| commit | aca9c227772e3765833605866ac413e61a98d04a (patch) | |
| tree | bb83f43b1ebf846f32429fbcdebd782bf843c51c /doc/refman/RefMan-ltac.tex | |
| parent | e0ff9328c51cec3bd65d4893af5da5c9f8ba2570 (diff) | |
Silence some warning about references in documentation.
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 13b2d387b..c924c02eb 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -27,7 +27,7 @@ problems. \def\cpattern{\nterm{cpattern}} The syntax of the tactic language is given Figures~\ref{ltac} -and~\ref{ltac_aux}. See Chapter~\ref{BNF-syntax} for a description of +and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this chapter: entries {\naturalnumber}, {\integer}, {\ident}, {\qualid}, {\term}, @@ -187,7 +187,7 @@ is understood as \end{tabular} \end{centerframe} \caption{Syntax of the tactic language (continued)} -\label{ltac_aux} +\label{ltac-aux} \end{figure} \begin{figure}[ht] |