Reworking error message for unresolved evar subterm of another evar.

This is a reworking of 7fd28dc9: instead of using words such as
"domain of", "codomain of" to refer to a position in the instance of
the original evar, we simply display the instance and the name of the
unresolved evar in this instance. This is both simpler and more
informative. (The positional words remain useful for printing the
evar_map in debugging though.)

In passing, this fixes #8369 (Not_found in printing message about an
unresolved subevar).

Incidentally add possible breaking while printing "in environment".

1 files changed, 12 insertions, 12 deletions

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