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.

17 files changed, 40 insertions, 37 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 59c24900d..2644a56b3 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,7 +17,7 @@ open Decl_kinds
 (***********************)
 (* For binders parsing *)
 
-let binding_kind_eq bk1 bk2 = match bk1, bk2 with
+let implicit_status_eq bk1 bk2 = match bk1, bk2 with
 | Explicit, Explicit -> true
 | Implicit, Implicit -> true
 | _ -> false
@@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
 | _ -> false
 
 let binder_kind_eq b1 b2 = match b1, b2 with
-| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2
 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
-  binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+  implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 &&
   (if b1 then b2 else not b2)
 | _ -> false
 
@@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 =
   | CPrim(_,i1), CPrim(_,i2) ->
     prim_token_eq i1 i2
   | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
-    binding_kind_eq bk1 bk2 &&
+    implicit_status_eq bk1 bk2 &&
     Option.equal abstraction_kind_eq ak1 ak2 &&
     constr_expr_eq e1 e2
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f..bfe546ba5 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
 val local_binder_eq : local_binder -> local_binder -> bool
 (** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
 
-val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
-(** Equality on [binding_kind] *)
+val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool
+(** Equality on [implicit_status] *)
 
 val binder_kind_eq : binder_kind -> binder_kind -> bool
 (** Equality on [binder_kind] *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f7fcbb4ee..62cb62f49 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c =
   let c = extern_typ scopes vars c in
   match na, c with
   | Name id, CProdN (loc,[nal,Default bk',ty],c)
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
+      when implicit_status_eq bk bk' && constr_expr_eq aty ty
       && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
@@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
   let c = sub_extern inctx scopes vars c in
   match c with
   | CLambdaN (loc,[nal,Default bk',ty],c)
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
+      when implicit_status_eq bk bk' && constr_expr_eq aty ty
       && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fb11359e3..b9f5704d8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -65,7 +65,7 @@ type var_internalization_data =
 type internalization_env =
     (var_internalization_data) Id.Map.t
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
 
 type ltac_sign = {
   ltac_vars : Id.Set.t;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index eea76aa31..718aa753e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -75,7 +75,7 @@ type ltac_sign = {
 
 val empty_ltac_sign : ltac_sign
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6b29b6d3d..c65d43db3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
       on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
   | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
@@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
-    let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
+    let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in
     let unify_binder alp b b' =
       match b, b' with
       | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
+         alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t')
       | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
+         alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t')
       | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
          let alp, p = unify_pat alp p p' in
-         alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+         alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -1122,7 +1122,7 @@ let term_of_binder = function
   | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
 type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+    (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
       glob_constr option * glob_constr
 
 let match_notation_constr u c (metas,pat) =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 854e222e3..6428ccab6 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 exception No_match
 
 type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+    (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
       glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575..e494b2f81 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -23,8 +23,8 @@ type explicitation =
   | ExplByName of Id.t
 
 type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
+  | Default of implicit_status
+  | Generalized of implicit_status * implicit_status * bool
       (** Inner binding, outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
@@ -95,7 +95,7 @@ and constr_expr =
   | CSort of Loc.t * glob_sort
   | CCast of Loc.t * constr_expr * constr_expr cast_type
   | CNotation of Loc.t * notation * constr_notation_substitution
-  | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
+  | CGeneralization of Loc.t * implicit_status * abstraction_kind option * constr_expr
   | CPrim of Loc.t * prim_token
   | CDelimiters of Loc.t * string * constr_expr
 
@@ -132,7 +132,7 @@ and constr_notation_substitution =
     constr_expr list list * (** for recursive notations *)
     local_binder list list (** for binders subexpressions *)
 
-type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * implicit_status * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 29972f2f4..c117baf3f 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -10,7 +10,10 @@
 
 type locality = Discharge | Local | Global
 
-type binding_kind = Explicit | Implicit
+type implicit_status = Explicit | Implicit
+
+type binding_kind = implicit_status
+(** @deprecated Alias type *)
 
 type polymorphic = bool
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b3159c860..178952fef 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -40,8 +40,8 @@ type glob_constr =
   | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
   | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
   | GApp of Loc.t * glob_constr * glob_constr list
-  | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
-  | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLambda of Loc.t * Name.t * implicit_status *  glob_constr * glob_constr
+  | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr
   | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
@@ -54,7 +54,7 @@ type glob_constr =
   | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option)
   | GCast of Loc.t * glob_constr * glob_constr cast_type
 
-and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
+and glob_decl = Name.t * implicit_status * glob_constr option * glob_constr
 
 and fix_recursion_order =
   | GStructRec
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
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 004dd6801..b1b8aa288 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -241,7 +241,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind }
           let k = IsAssumption Conjectural in
           let c = SectionLocalAssum { type_context = (t_i,ctx);
                                       polymorphic;
-                                      binding_kind = impl }
+                                      implicit_status = impl }
           in
           let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 40c65b56f..7bb016d34 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -230,7 +230,7 @@ let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident)
   | Discharge when Lib.sections_are_opened () ->
      let entry = SectionLocalAssum { type_context = (c,ctx);
                                      polymorphic;
-                                     binding_kind = impl }
+                                     implicit_status = impl }
      in
      let decl = (Lib.cwd(), entry, IsAssumption kind) in
      let _ = declare_variable ident decl in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2ae4cddd0..f0651a98c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -55,7 +55,7 @@ val do_definition : Id.t -> definition_kind -> lident list option ->
 val declare_assumption : coercion_flag -> assumption_kind -> 
   types Univ.in_universe_context_set ->
   Universes.universe_binders -> Impargs.manual_implicits ->
-  binding_kind -> Vernacexpr.inline -> variable Loc.located ->
+  implicit_status -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : assumption_kind ->