Merge PR #10665: [api] Move handling of variable implicit data to impargs

Reviewed-by: SkySkimmer

42 files changed, 67 insertions, 97 deletions

diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
new file mode 100644
index 0000000000..0c47f6a60b
--- /dev/null
+++ b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then
+
+    elpi_CI_REF=api+varkind
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    quickchick_CI_REF=api+varkind
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
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
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
deleted file mode 100644
index 17746645ee..0000000000
--- a/library/decl_kinds.ml
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-type binding_kind = Explicit | Implicit
diff --git a/library/lib.ml b/library/lib.ml
index 6b01eb07e9..3f51826315 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -441,9 +441,6 @@ let empty_section_data ~poly = {
 let sectab =
   Summary.ref ([] : section_data list) ~name:"section-context"
 
-let sec_implicits =
-  Summary.ref Id.Map.empty ~name:"section-implicits"
-
 let check_same_poly p sec =
   if p != sec.sec_poly then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
@@ -452,14 +449,13 @@ let add_section ~poly () =
   List.iter (fun tab -> check_same_poly poly tab) !sectab;
   sectab := empty_section_data ~poly :: !sectab
 
-let add_section_variable ~name ~kind ~poly =
+let add_section_variable ~name ~poly =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | s :: sl ->
        List.iter (fun tab -> check_same_poly poly tab) !sectab;
        let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
-       sectab := s :: sl;
-       sec_implicits := Id.Map.add name kind !sec_implicits
+       sectab := s :: sl
 
 let add_section_context ctx =
   match !sectab with
@@ -576,8 +572,6 @@ let section_segment_of_reference = let open GlobRef in function
 let variable_section_segment_of_reference gr =
   (section_segment_of_reference gr).abstr_ctx
 
-let variable_section_kind id = Id.Map.get id !sec_implicits
-
 let section_instance = let open GlobRef in function
   | VarRef id ->
      let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index 7dc8b52282..9ffa69ef93 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -177,12 +177,11 @@ val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
 val section_segment_of_reference : GlobRef.t -> abstr_info
 
 val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
-val variable_section_kind : Id.t -> Decl_kinds.binding_kind
 
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit
+val add_section_variable : name:Id.t -> poly:bool -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
 val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
diff --git a/library/library.mllib b/library/library.mllib
index 84937ede93..3b75438ccd 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,4 +1,3 @@
-Decl_kinds
 Libnames
 Globnames
 Libobject
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 78a12a2e7d..ea44e748c9 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -19,7 +19,6 @@ open Constrexpr_ops
 open Util
 open Tok
 open Namegen
-open Decl_kinds
 
 open Pcoq
 open Pcoq.Prim
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 730ae48393..a836335d4d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1600,7 +1600,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
         let b = Names.Id.of_string "___b" in
         Constrexpr_ops.mkLambdaC(
           [CAst.make @@ Name a; CAst.make @@ Name b],
-          Constrexpr.Default Decl_kinds.Explicit,
+          Constrexpr.Default Glob_term.Explicit,
           wf_arg_type,
           Constrexpr_ops.mkAppC(wf_rel_expr,
                                 [
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6eb8c42d1d..ddd6ecfb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt =
     | Constrexpr.CLetIn(na,v,t,t') ->
         CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
     | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
-                                       Constrexpr.Default Decl_kinds.Explicit, rt)],
+                                       Constrexpr.Default Explicit, rt)],
                              CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true}))
 
 let do_build_inductive
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index d36d86a65b..fbf63c69dd 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -4,7 +4,6 @@ open Glob_term
 open CErrors
 open Util
 open Names
-open Decl_kinds
 
 (*
    Some basic functions to rebuild glob_constr
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7cd43cb5cd..9b52b710c1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -24,7 +24,6 @@ open Tactypes
 open Tactics
 open Inv
 open Locus
-open Decl_kinds
 
 open Pcoq
 
@@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram
       | -> { true } ] ]
   ;
   simple_binder:
-    [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+    [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@
                     CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
-      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
+      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) }
     ] ]
   ;
   fixdecl:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 0e38ce575b..6df068883c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,7 +20,6 @@ open Stdarg
 open Notation_gram
 open Tactypes
 open Locus
-open Decl_kinds
 open Genredexpr
 open Ppconstr
 open Pputils
@@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
         match DAst.get ty with
-            Glob_term.GProd(na,Explicit,a,b) ->
+            Glob_term.GProd(na,Glob_term.Explicit,a,b) ->
               strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 33e9f871fd..473612fda7 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
 
 (** Constructors for rawconstr *)
 open Glob_term
-open Decl_kinds
 
 let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 175a863ad8..a1f707ffa8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -32,7 +32,6 @@ open Ppconstr
 
 open Namegen
 open Tactypes
-open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
 
@@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
  | [ ssrbvar(bv) ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ")" ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
    { let x = bvar_lname bv in
      (FwdPose, [BFdecl 1]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
    { let xs = List.map bvar_lname (bv :: bvs) in
      let n = List.length xs in
      (FwdPose, [BFdecl n]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
    { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram
   ssrbinder: [
   [  ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
   ];
 END
 
@@ -1391,7 +1390,7 @@ let push_binders c2 bs =
 
 let rec fix_binders = let open CAst in function
   | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
-      CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
+      CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
   | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
     CLocalDef (x, v, oty) :: fix_binders bs
   | _ -> []
@@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function
   | IPatId id ->
       let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
-        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
+        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
           mkCHole None)
   | _ -> anomaly "non-id accepted as binder")
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0adabb0673..f3f1d713e9 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -27,7 +27,6 @@ open Notation_ops
 open Notation_term
 open Glob_term
 open Stdarg
-open Decl_kinds
 open Pp
 open Ppconstr
 open Printer
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 17db25660f..4d7a04f5ee 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -36,7 +36,6 @@ open Ppconstr
 open Printer
 open Globnames
 open Namegen
-open Decl_kinds
 open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index a148a3bc73..9808c61255 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts =
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
   let arrow x y =
-    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+    mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
   in
   let opt r = app (mkRefC (q_option ())) r in
   let constructors = get_constructors tyc in
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 8c0f9a3339..c92acb0f55 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope =
   let of_ty = Smartlocate.global_with_alias g in
   let cty = cref ty in
   let arrow x y =
-    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+    mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
   in
   let constructors = get_constructors tyc in
   (* Check the type of f *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2061b41292..e8c83c7de9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,7 +25,6 @@ open Namegen
 open Libnames
 open Globnames
 open Mod_subst
-open Decl_kinds
 open Context.Named.Declaration
 open Ltac_pretype
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cc9f520583..9eb014aa62 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -57,10 +57,10 @@ val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (
 
 val share_pattern_names :
   (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
-  (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list ->
+  (Name.t * binding_kind * 'b option * 'a) list ->
   Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
   Pattern.constr_pattern ->
-  (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a
+  (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a
 
 val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6bde3dfd81..93f5923474 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -67,9 +67,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
   | (UNamed _ | UAnonymous _), _ -> false
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
-  | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
-  | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
-  | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
+  | Explicit, Explicit -> true
+  | Implicit, Implicit -> true
+  | (Explicit | Implicit), _ -> false
 
 let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 467b72e520..37aa31d094 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -48,6 +48,9 @@ val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_const
 val map_glob_constr :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
+(** Equality on [binding_kind] *)
+val binding_kind_eq : binding_kind -> binding_kind -> bool
+
 (** Ensure traversal from left to right *)
 val map_glob_constr_left_to_right :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 7c859a5332..10e9d60fd5 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -17,7 +17,6 @@
    arguments and pattern-matching compilation are not. *)
 
 open Names
-open Decl_kinds
 
 type existential_name = Id.t
 
@@ -66,6 +65,8 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
 
 type cases_pattern = [ `any ] cases_pattern_g
 
+type binding_kind = Explicit | Implicit
+
 (** Representation of an internalized (or in other words globalized) term. *)
 type 'a glob_constr_r =
   | GRef of GlobRef.t * glob_level list option
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99e3c5025e..ccc3b6e83c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Context
 open Glob_term
 open Pp
 open Mod_subst
-open Decl_kinds
 open Pattern
 open Environ
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c28c3ab730..4fed526cfc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1193,7 +1193,7 @@ let path_convertible env sigma p q =
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
   let mkGApp(rt,rtl)      = DAst.make @@ Glob_term.GApp(rt,rtl) in
-  let mkGLambda(n,t,b)    = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in
+  let mkGLambda(n,t,b)    = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in
   let mkGHole ()          = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
   let path_to_gterm p =
     match p with
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index aea4f23205..5ed96dd5e3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -21,7 +21,6 @@ open Glob_term
 open Constrexpr
 open Constrexpr_ops
 open Notation_gram
-open Decl_kinds
 open Namegen
 (*i*)
 
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 391524ebda..c280760e84 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -300,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
+  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
@@ -317,7 +317,6 @@ let declare_variable ~name ~kind d =
     | SectionLocalAssum {typ;univs;poly;impl} ->
       let () = declare_universe_context ~poly univs in
       let () = Global.push_named_assum (name,typ) in
-      let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in
       impl, true, poly
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
@@ -342,14 +341,14 @@ let declare_variable ~name ~kind d =
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      Decl_kinds.Explicit, de.proof_entry_opaque,
+      Glob_term.Explicit, de.proof_entry_opaque,
       poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~kind:impl ~poly;
+  add_section_variable ~name ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
-  Impargs.declare_var_implicits name;
+  Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
 (** Declaration of inductive blocks *)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 89b41076f7..4ae9f6c7ae 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,7 +23,7 @@ open Entries
 
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a Proof_global.proof_entry
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a3a88df21e..61e0e41eb9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -258,7 +258,6 @@ type equation_kind =
 exception NoEquationFound
 
 open Glob_term
-open Decl_kinds
 open Evar_kinds
 
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 075d89d0df..d5f5656e1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,9 +28,7 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 (*i*)
 
-open Decl_kinds
-
-let set_typeclass_transparency c local b = 
+let set_typeclass_transparency c local b =
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
 
@@ -527,7 +525,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
 let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass =
-    if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
+    if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
     else tclass
   in
   let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 7d365db85c..e3f90ab98c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -100,7 +100,7 @@ let next_uctx =
 let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
   let refs, _ =
     List.fold_left (fun (refs,uctx) id ->
-        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
+        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in
         ref::refs, next_uctx uctx)
       ([],uctx) idl
   in
@@ -292,7 +292,7 @@ let context ~poly l =
         | Some (Name id',_) -> Id.equal name id'
         | _ -> false
       in
-      let impl = List.exists test impls in
+      let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in
       let scope =
         if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
       match b with
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 1632c3d578..2715bd8305 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -34,7 +34,7 @@ val declare_assumption
   -> Entries.universes_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
-  -> bool (** implicit *)
+  -> Glob_term.binding_kind
   -> Declaremods.inline
   -> variable CAst.t
   -> GlobRef.t * Univ.Instance.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index adfb058942..7809425a10 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -258,7 +258,7 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect
     let open DeclareDef in
     (match scope with
      | Discharge ->
-       let impl = false in (* copy values from Vernacentries *)
+       let impl = Glob_term.Explicit in
        let univs = match univs with
          | Polymorphic_entry (_, univs) ->
            (* What is going on here? *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d4b2029e99..b712d7e264 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -170,7 +170,7 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder_expr list * constr_expr option * constructor_expr list
 
-type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
+type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list
 
 type proof_expr =