diff options
| author | Pierre-Marie Pédrot | 2020-03-11 11:29:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 245b94cd075b6be527590c425a98262d89577909 (patch) | |
| tree | 0e989e6db3f1e113cc0bb59c92f6e88424f92b79 /pretyping/typeclasses.ml | |
| parent | 693c0fb3ad7344aadc840ab7124782e64997b739 (diff) | |
Hack a non-superglobal mode for hints.
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index aa2e96c2d7..d4f59d7a36 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -34,9 +34,6 @@ let get_typeclasses_unique_solutions = ~key:["Typeclasses";"Unique";"Solutions"] ~value:false -let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make () -let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c - let (classes_transparent_state, classes_transparent_state_hook) = Hook.make () let classes_transparent_state () = Hook.get classes_transparent_state () |