From 43c712d85d636b797766744907353521f408331c Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 5 Sep 2014 09:53:09 +0200
Subject: Ltac's [uconstr] values now use the identifier context to give names
 to binders.

It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.---
 intf/glob_term.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ec27aab338..b4543bb59b 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -77,6 +77,7 @@ and cases_clauses = cases_clause list
     of its free variables. Intended for use when these variables are taken
     from the Ltac environment. *)
 type closure = {
+  idents:Id.t Id.Map.t;
   typed: Pattern.constr_under_binders Id.Map.t ;
   untyped:closed_glob_constr Id.Map.t }
 and closed_glob_constr = {
-- 
cgit v1.2.3