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.
---
 intf/evar_kinds.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index afc5e3bab9..470ad2a23b 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -20,6 +20,7 @@ type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of obligation_definition_status
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
-- 
cgit v1.2.3