diff options
| author | Maxime Dénès | 2018-11-13 10:11:15 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-26 08:51:00 +0000 |
| commit | e9bbfcd6d589a9e8e5abcd9fbc852a77996c97db (patch) | |
| tree | e293ad303dada2a0fa768c73f3ea79e2721f1c48 /plugins/ltac/g_class.mlg | |
| parent | b87f1432474bd3ffda6f02eb3ba7edf50114cc23 (diff) | |
Declare initial hint databases in prelude
Previously, they were hard-wired in the ML code.
Diffstat (limited to 'plugins/ltac/g_class.mlg')
| -rw-r--r-- | plugins/ltac/g_class.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
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 |