Merge pull request #118 from vbgl/rm-hardwired-hint-db

Fix for coq/coq#8984
coq · Apr 2, 2019 · f1530a7 · f1530a7
2 parents a41b22a + e80464b
commit f1530a7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
@@ -405,7 +405,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