diff options
| author | Matthieu Sozeau | 2014-09-19 21:10:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-19 21:15:22 +0200 |
| commit | e8726550e01e51ef3ccf8602f2ecbe2b3737cca3 (patch) | |
| tree | 86b5f6eec7633fb17c01206e9cc7e2f16ec2060b /kernel/nativecode.mli | |
| parent | 9c2bbdd58b6935ea980e72289777a20b85fe4fdb (diff) | |
Move the specific map_constr_with_binders_left_to_right
for e_contextually where it is used. Bug #3648 is fixed.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions