3 files changed, 8 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b1e12bd66e..38f9b57e45 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2339,7 +2339,7 @@ let extract_ids env =
 let scope_of_type_kind sigma = function
   | IsType -> Notation.current_type_scope_name ()
   | OfType typ -> compute_type_scope sigma typ
-  | WithoutTypeConstraint -> None
+  | WithoutTypeConstraint | UnknownIfTermOrType -> None
 
 let empty_ltac_sign = {
   ltac_vars = Id.Set.empty;
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