diff options
| author | Maxime Dénès | 2014-10-24 00:10:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2014-10-24 00:10:38 +0200 |
| commit | 6f6eaa858a2a4268b8c6a63a284e9d07941b511f (patch) | |
| tree | 6e83cf5fa9729ddcacc3518e4ae0fee9a629c496 /kernel/type_errors.mli | |
| parent | 89eaab788fafcadaf5fe5fca8100bddd54675395 (diff) | |
No hash consing across calls to the native compiler.
The induced side effects were incompatible with the undo machinery.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions