From e9bbfcd6d589a9e8e5abcd9fbc852a77996c97db Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 13 Nov 2018 10:11:15 +0100
Subject: Declare initial hint databases in prelude

Previously, they were hard-wired in the ML code.
---
 plugins/ltac/g_class.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 3f2fabeeee..049a699cbd 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto
  | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     { typeclasses_eauto ~depth:d l }
  | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
-     typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] }
+     typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
 END
 
 TACTIC EXTEND head_of_constr
-- 
cgit v1.2.3