diff options
| author | Théo Zimmermann | 2020-03-18 17:11:03 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-18 17:11:03 +0100 |
| commit | 55490662517966d01a53ddd708709d1fc739286c (patch) | |
| tree | 368e941af3ca3d63de2921bb59ace8ac88e6e5a8 /pretyping | |
| parent | 4c2a4890b75d516acfeccdb4105e46760239a7f1 (diff) | |
| parent | c685a8a3690b3345dbc2770530e3da1b6639a654 (diff) | |
Merge PR #11812: Add an Export locality to hints
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes
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 |