diff options
| author | Pierre-Marie Pédrot | 2019-04-02 18:38:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-02 18:38:06 +0200 |
| commit | 97edaec1d6df277da0e44d9b99abc2fdd309bfd6 (patch) | |
| tree | 4442af9250415a203a2b137ce87b0f989e442e80 /vernac/classes.ml | |
| parent | 974dc811fe30a762235b68fb3c0ac5c3eeca45b9 (diff) | |
| parent | 388ed80af0826997718565c8101105b372e99fa8 (diff) | |
Merge PR #8984: Declare initial hint databases in prelude
Ack-by: JasonGross
Reviewed-by: ppedrot
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 6a67a1b5d0..d61d324941 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 |