diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-09 13:00:02 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-09 13:10:44 +0200 |
| commit | 7a037b8c1de11b18d47b01e5b0262090f32bfc40 (patch) | |
| tree | 208d8bca22e7edc81a80dfedacf8eb5244db83bc /pretyping/typing.mli | |
| parent | 53b2acb9befe13c0383b923d09a0d5a6c416449e (diff) | |
Restore native compiler optimizations after they were broken by 9e2ee58.
The greatest danger of OCaml's polymorphic equality is that PMP can
replace it with pointer equality at any time, be warned :)
The lack of optimization may account for an exponential blow-up in size
of the generated code, as well as worse runtime performance.
Diffstat (limited to 'pretyping/typing.mli')
0 files changed, 0 insertions, 0 deletions