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".

2 files changed, 8 insertions, 4 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