diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-15 14:28:35 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-15 15:44:10 +0200 |
| commit | 006c487f8af220cf8a374bc38d06c3d58fe4335b (patch) | |
| tree | e1f7c58a6c6ae4ef1fe9d45b207ee709747bb320 /interp/constrintern.mli | |
| parent | 708f0634b75b784f9196d063edd19274bbb43425 (diff) | |
Fix a bug in the naming of binders.
The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
Diffstat (limited to 'interp/constrintern.mli')
0 files changed, 0 insertions, 0 deletions