From d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Jan 2017 15:05:08 +0100
Subject: Adding a new evar source to remember the name of evars which were
 named in the original term.

Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
---
 toplevel/himsg.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 891662b93a..6cff805fc2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -532,6 +532,8 @@ let pr_trailing_ne_context_of env sigma =
   else (str " in environment:"++ pr_context_unlimited env sigma)
 
 let rec explain_evar_kind env sigma evk ty = function
+  | Evar_kinds.NamedHole id ->
+      strbrk "the existential variable named " ++ pr_id id
   | Evar_kinds.QuestionMark _ ->
       strbrk "this placeholder of type " ++ ty
   | Evar_kinds.CasesType false ->
-- 
cgit v1.2.3