Merge PR #8373: Fixes #8369: Not_found in printing message about an unresolved subevar.

3 files changed, 20 insertions, 16 deletions

diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v
new file mode 100644
index 0000000000..9816954d0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8369.v
@@ -0,0 +1,3 @@
+(* Was failing in master with a not_found generated by the printer *)
+
+Fail Definition foo := fun '(u, v) p2 => (u, v).
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index cf2d5b2850..14c48e8fa0 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -9,10 +9,11 @@ The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Instance is not well-typed in the environment of ?x.
 The command has indeed failed with message:
-Cannot infer the domain of the type of f.
+Cannot infer ?T in the partial instance "?T -> nat" found for the type of f.
 The command has indeed failed with message:
-Cannot infer the domain of the implicit parameter A of id whose type is
-"Type".
+Cannot infer ?T in the partial instance "?T -> nat" found for the implicit
+parameter A of id whose type is "Type".
 The command has indeed failed with message:
-Cannot infer the codomain of the type of f in environment:
+Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the
+type of f in environment:
 x : nat
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a2b5c8d70a..f3e1e1fc49 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -511,7 +511,7 @@ let pr_trailing_ne_context_of env sigma =
   if List.is_empty (Environ.rel_context env) &&
     List.is_empty (Environ.named_context env)
   then str "."
-  else (str " in environment:"++ pr_context_unlimited env sigma)
+  else (strbrk " in environment:" ++ pr_context_unlimited env sigma)
 
 let rec explain_evar_kind env sigma evk ty =
     let open Evar_kinds in
@@ -551,21 +551,21 @@ let rec explain_evar_kind env sigma evk ty =
       strbrk "an instance of type " ++ ty ++
       str " for the variable " ++ Id.print id
   | Evar_kinds.SubEvar (where,evk') ->
-      let evi = Evd.find sigma evk' in
+      let rec find_source evk =
+        let evi = Evd.find sigma evk in
+        match snd evi.evar_source with
+        | Evar_kinds.SubEvar (_,evk) -> find_source evk
+        | src -> evi,src in
+      let evi,src = find_source evk' in
       let pc = match evi.evar_body with
       | Evar_defined c -> pr_leconstr_env env sigma c
       | Evar_empty -> assert false in
       let ty' = evi.evar_concl in
-      (match where with
-      | Some Evar_kinds.Body -> str "the body of "
-      | Some Evar_kinds.Domain -> str "the domain of "
-      | Some Evar_kinds.Codomain -> str "the codomain of "
-      | None ->
-      pr_existential_key sigma evk ++ str " of type " ++ ty ++
-      str " in the partial instance " ++ pc ++
-      str " found for ") ++
-      explain_evar_kind env sigma evk'
-      (pr_leconstr_env env sigma ty') (snd evi.evar_source)
+      pr_existential_key sigma evk ++
+      strbrk " in the partial instance " ++ pc ++
+      strbrk " found for " ++
+      explain_evar_kind env sigma evk
+      (pr_leconstr_env env sigma ty') src
 
 let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr sigma evi.evar_concl with