aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2016-11-17 16:01:29 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2016-11-17 16:01:29 +0100
commit253493355a71c0673b0c10b06e7eb9f0fd0242a9 (patch)
tree7afb701fc537f5662c0627ebbfedcca5583f42b1 /doc
parent81c9fa0de99400b51c029cdbd1519b4f724e320a (diff)
Add missing label. Fixes broken ref.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Classes.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index bd8ee450e..acfc4bea9 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}).
\asubsection{\tt typeclasses eauto}
\tacindex{typeclasses eauto}
+\label{typeclasseseauto}
The {\tt typeclasses eauto} tactic uses a different resolution engine
than {\tt eauto} and {\tt auto}. The main differences are the following: