[api] Move handling of variable implicit data to impargs

We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.

This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.

We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.

9 files changed, 18 insertions, 27 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index e4af0fcee0..49b9149675 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Libnames
-open Decl_kinds
 
 (** {6 Concrete syntax for terms } *)
 
@@ -39,8 +38,8 @@ type explicitation =
   | ExplByName of Id.t
 
 type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * bool
+  | Default of Glob_term.binding_kind
+  | Generalized of Glob_term.binding_kind * bool
       (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
@@ -121,7 +120,7 @@ and constr_expr_r =
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation * constr_notation_substitution
-  | CGeneralization of binding_kind * abstraction_kind option * constr_expr
+  | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
   | CDelimiters of string * constr_expr
 and constr_expr = constr_expr_r CAst.t
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8fce24249c..3f216b0d63 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,25 +17,19 @@ open Namegen
 open Glob_term
 open Constrexpr
 open Notation
-open Decl_kinds
 
 (***********************)
 (* For binders parsing *)
 
-let binding_kind_eq bk1 bk2 = match bk1, bk2 with
-| Explicit, Explicit -> true
-| Implicit, Implicit -> true
-| _ -> false
-
 let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
 | AbsLambda, AbsLambda -> true
 | AbsPi, AbsPi -> true
 | _ -> false
 
 let binder_kind_eq b1 b2 = match b1, b2 with
-| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Default bk1, Default bk2 -> Glob_ops.binding_kind_eq bk1 bk2
 | Generalized (ck1, b1), Generalized (ck2, b2) ->
-  binding_kind_eq ck1 ck2 &&
+  Glob_ops.binding_kind_eq ck1 ck2 &&
   (if b1 then b2 else not b2)
 | _ -> false
 
@@ -172,7 +166,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 &&
+      Glob_ops.binding_kind_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 3ed240d356..a05a9cb999 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -26,9 +26,6 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
 val local_binder_eq : local_binder_expr -> local_binder_expr -> bool
 (** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *)
 
-val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
-(** Equality on [binding_kind] *)
-
 val binder_kind_eq : binder_kind -> binder_kind -> bool
 (** Equality on [binder_kind] *)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 96392edb11..217381d854 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -27,7 +27,6 @@ open Glob_ops
 open Pattern
 open Notation
 open Detyping
-open Decl_kinds
 
 module NamedDecl = Context.Named.Declaration
 (*i*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f341071728..f2cb4ae5c7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -31,7 +31,6 @@ open Notation_term
 open Notation_ops
 open Notation
 open Inductiveops
-open Decl_kinds
 open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3f2a1b075c..5f41c2a366 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Globnames
 open Declarations
-open Decl_kinds
 open Lib
 open Libobject
 open EConstr
@@ -486,12 +485,17 @@ let subst_implicits_decl subst (r,imps as o) =
 let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
 
+(* This was moved out of lib.ml, however it is not stored with regular
+   implicit data *)
+let sec_implicits =
+  Summary.ref Id.Map.empty ~name:"section-implicits"
+
 let impls_of_context ctx =
   let map decl =
     let id = NamedDecl.get_id decl in
-    match Lib.variable_section_kind id with
-    | Implicit -> Some (id, Manual, (true, true))
-    | _ -> None
+    match Id.Map.get id !sec_implicits with
+    | Glob_term.Implicit -> Some (id, Manual, (true, true))
+    | Glob_term.Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
 
@@ -579,9 +583,10 @@ let declare_implicits local ref =
     if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in
     declare_implicits_gen req flags ref
 
-let declare_var_implicits id =
+let declare_var_implicits id ~impl =
   let flags = !implicit_args in
-    declare_implicits_gen ImplLocal flags (GlobRef.VarRef id)
+  sec_implicits := Id.Map.add id impl !sec_implicits;
+  declare_implicits_gen ImplLocal flags (GlobRef.VarRef id)
 
 let declare_constant_implicits con =
   let flags = !implicit_args in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 90a7944642..2751b9d40b 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -93,7 +93,7 @@ val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list
 
 (** {6 Computation of implicits (done using the global environment). } *)
 
-val declare_var_implicits : variable -> unit
+val declare_var_implicits : variable -> impl:Glob_term.binding_kind -> unit
 val declare_constant_implicits : Constant.t -> unit
 val declare_mib_implicits : MutInd.t -> unit
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 9f6281ae15..455471a472 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Context
-open Decl_kinds
 open CErrors
 open Util
 open Glob_term
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2fa78bb9f3..f30a874426 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -15,7 +15,6 @@ open Names
 open Nameops
 open Constr
 open Globnames
-open Decl_kinds
 open Namegen
 open Glob_term
 open Glob_ops