diff options
| author | Pierre-Marie Pédrot | 2015-10-26 14:35:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-27 00:07:14 +0100 |
| commit | 9b2bb33662a4a1e39202cb81f894b739782c3434 (patch) | |
| tree | a639a0ac146e81ceeb0b075b3551a3f2c3913b9d /kernel/nativecode.mli | |
| parent | fb50a8aaf8826349ac8c3a90a6d9b354b9cf34ca (diff) | |
Indexing existentially quantified entries returned by interp_entry_name.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions