Slightly refining some error messages about unresolvable evars.

For instance, error in "Goal forall a f, f a = 0" is now located.

1 files changed, 6 insertions, 2 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 3dfb0c34f..b7531f6fc 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -206,8 +206,12 @@ let pr_evar_source = function
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id
-  | Evar_kinds.SubEvar evk ->
-    str "subterm of " ++ Evar.print evk
+  | Evar_kinds.SubEvar (where,evk) ->
+     (match where with
+     | None -> str "subterm of "
+     | Some Evar_kinds.Body -> str "body of "
+     | Some Evar_kinds.Domain -> str "domain of "
+     | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
 
 let pr_evar_info evi =
   let open Evd in