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.

4 files changed, 8 insertions, 8 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 36a58629e..5c6543e28 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -46,7 +46,7 @@ type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
                            polymorphic : bool;
-                           binding_kind : binding_kind }
+                           implicit_status : implicit_status }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
@@ -59,9 +59,9 @@ let cache_variable ((sp,_),o) =
     alreadydeclared (pr_id id ++ str " already exists");
 
   let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum { type_context = (ty,ctx); polymorphic; binding_kind } ->
+    | SectionLocalAssum { type_context = (ty,ctx); polymorphic; implicit_status } ->
       let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in
-	binding_kind, true, polymorphic, ctx
+	implicit_status, true, polymorphic, ctx
     | SectionLocalDef (de) ->
       let univs = Global.push_named_def (id,de) in
       Explicit, de.const_entry_opaque,
diff --git a/library/declare.mli b/library/declare.mli
index 760bf437b..a0ec26444 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -25,7 +25,7 @@ type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
                            polymorphic : bool;
-                           binding_kind : binding_kind }
+                           implicit_status : implicit_status }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
diff --git a/library/lib.ml b/library/lib.ml
index 954889fb6..13921610d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -391,7 +391,7 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-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
@@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+  | Variable of (Names.Id.t * Decl_kinds.implicit_status *
 		   Decl_kinds.polymorphic * Univ.universe_context_set)
   | Context of Univ.universe_context_set
 
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