From 0703cd1bbe5aab7e584d2293fe76c5f6ac4fe08c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Aug 2018 18:51:04 +0200
Subject: 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".
---
 test-suite/bugs/closed/bug_8369.v |  3 +++
 test-suite/output/Errors.out      |  9 +++++----
 vernac/himsg.ml                   | 24 ++++++++++++------------
 3 files changed, 20 insertions(+), 16 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_8369.v

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
-- 
cgit v1.2.3