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 | |
| 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')
| -rw-r--r-- | pretyping/typeclasses.ml | 3 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
2 files changed, 0 insertions, 6 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 () diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2715c1eda5..c350f97107 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -122,9 +122,6 @@ val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr -val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t -val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit - val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t val classes_transparent_state : unit -> TransparentState.t |