From 1bc1cba7a759a285131a3ed6ea8979716700b856 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 17:13:27 +0200 Subject: Rename Decl_kinds.binding_kind into Decls_kind.implicit_status. The new name makes it more obvious what is meant here by "kind". We leave Decl_kinds.binding_kind as a deprecated alias for plugin compatibility. We also replace bool with implicit_status in a few places in the codebase. --- library/lib.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index e905ee57e..51c74d395 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,7 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -176,7 +176,7 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.implicit_status -> polymorphic:bool -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : polymorphic:bool -> Names.constant -> Context.Named.t -> unit -- cgit v1.2.3