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.
---
 engine/evd.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index bffb407274..7006fde3cc 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1299,6 +1299,7 @@ let pr_decl (decl,ok) =
                            print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
+  | Evar_kinds.NamedHole id -> pr_id id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
-- 
cgit v1.2.3