diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-08-31 17:22:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-08-31 17:22:56 +0200 |
| commit | 06b871974ae222f878142c8cab03fd52d4511895 (patch) | |
| tree | 1deafb887d1eca4a1c15a5727648400a4ff909ec /doc | |
| parent | bdaf7032912feabf5ee97af33bf32e4359ad2d25 (diff) | |
RefMan-ssr: fix warning
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index 61f7421c4..0e4d44f21 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -91,7 +91,7 @@ logical view of a concept. To conclude it is worth mentioning that \ssr{} tactics can be mixed with non \ssr{} tactics in the same proof, or in the same LTac expression. The few exceptions -to this statement are described in section~\label{sec:compat}. +to this statement are described in section~\ref{sec:compat}. \iffalse %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |