4 files changed, 11 insertions, 6 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 02c2fc4a13..0969b3cc03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
-  | Implicit, Implicit -> true
-  | (Explicit | Implicit), _ -> false
+  | NonMaxImplicit, NonMaxImplicit -> true
+  | MaxImplicit, MaxImplicit -> true
+  | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
 
 let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 44323441b6..485a19421d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
 
 type cases_pattern = [ `any ] cases_pattern_g
 
-type binding_kind = Explicit | Implicit
+type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
 
 (** Representation of an internalized (or in other words globalized) term. *)
 type 'a glob_constr_r =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb0c4868b5..2d98d48aa0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,7 @@ open Evarconv
 
 module NamedDecl = Context.Named.Declaration
 
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint
 
 let (!!) env = GlobEnv.env env
 
@@ -1290,7 +1290,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
   in
   let env = GlobEnv.make ~hypnaming env sigma lvar in
   let sigma', c', c'_ty = match kind with
-    | WithoutTypeConstraint ->
+    | WithoutTypeConstraint | UnknownIfTermOrType ->
       let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18e416596e..ee57f690a1 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
 val search_guard :
   ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array
 
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint =
+  | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *)
+  | IsType (** Necessarily a type *)
+  | OfType of types (** A term of the expected type *)
+  | WithoutTypeConstraint (** A term of unknown expected type *)
 
 type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr