aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 44102afd74..a28f4597cf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -33,7 +33,8 @@ open Hints
module NamedDecl = Context.Named.Declaration
-(** Hint database named "typeclass_instances", now created directly in Auto *)
+(** Hint database named "typeclass_instances", created in prelude *)
+let typeclasses_db = "typeclass_instances"
(** Options handling *)