aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorMaxime Dénès2018-11-20 08:42:52 +0100
committerMaxime Dénès2018-11-20 08:42:52 +0100
commit4d26550af26c1dab464253cc470e8a876fee0025 (patch)
treef2594e7e0b7960c50d45d6cb2e782eb074d19150 /pretyping/typeclasses.mli
parent22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (diff)
parent4acdbe9be526dc7f646ab084e52fe4b9a6ad1399 (diff)
Merge PR #7925: Clean transparent state
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ee9c83dad3..8bdac0a575 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -119,8 +119,8 @@ val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types ->
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 -> transparent_state) Hook.t
-val classes_transparent_state : unit -> transparent_state
+val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
+val classes_transparent_state : unit -> TransparentState.t
val add_instance_hint_hook :
(global_reference_or_constr -> GlobRef.t list ->