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 /vernac/classes.ml | |
| parent | b87f1432474bd3ffda6f02eb3ba7edf50114cc23 (diff) | |
Declare initial hint databases in prelude
Previously, they were hard-wired in the ML code.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 1981e24ae4..6ce2a3f0a5 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -21,6 +21,7 @@ open Globnames open Constrintern open Constrexpr open Context.Rel.Declaration +open Class_tactics module RelDecl = Context.Rel.Declaration (*i*) @@ -38,12 +39,15 @@ let () = Goptions.(declare_bool_option { optwrite = (fun b -> refine_instance := b) }) -let typeclasses_db = "typeclass_instances" - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) - + +let classes_transparent_state () = + try + Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db) + with Not_found -> TransparentState.empty + let () = Hook.set Typeclasses.add_instance_hint_hook (fun inst path local info poly -> @@ -55,8 +59,7 @@ let () = (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst'])) ()); Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; - Hook.set Typeclasses.classes_transparent_state_hook - (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) + Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let intern_info {hint_priority;hint_pattern} = let env = Global.env() in |