diff options
| author | Arnaud Spiwack | 2014-09-05 09:53:09 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-05 18:26:00 +0200 |
| commit | 43c712d85d636b797766744907353521f408331c (patch) | |
| tree | d0fff9163c614ddda16a78172eb29eb7ffaed393 /intf | |
| parent | 2fcc458af16bbebb9748cb4220237e74452059fc (diff) | |
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.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/glob_term.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 = { |