From d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.
---
 interp/constrintern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 235e6e24f..c102d8e11 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1739,7 +1739,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let k = match k with
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-           Evar_kinds.QuestionMark st
+           (match naming with
+           | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+           | _ -> Evar_kinds.QuestionMark st)
         | Some k -> k
         in
         let solve = match solve with
-- 
cgit v1.2.3