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 /plugins/xml/doubleTypeInference.ml | |
| 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 'plugins/xml/doubleTypeInference.ml')
0 files changed, 0 insertions, 0 deletions