aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 059a1babd7..5d9b14eab0 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -404,7 +404,7 @@ let eauto debug n p lems dbs =
let typeclasses_eauto strategy depth dbs =
let only_classes, dbs = match dbs with
| None ->
- true, [Hints.typeclasses_db]
+ true, [Class_tactics.typeclasses_db]
| Some dbs ->
let dbs = List.map Id.to_string dbs in
false, dbs