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

Reviewed-by: SkySkimmer

5 files changed, 7 insertions, 9 deletions

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 =