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.mli | |
| 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.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |