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

Reviewed-by: SkySkimmer

7 files changed, 11 insertions, 9 deletions

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