diff options
| author | Pierre Letouzey | 2015-12-16 11:43:53 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-16 11:49:19 +0100 |
| commit | 53ab313dcf7ae524a9a8312658c1e9869a4039f7 (patch) | |
| tree | 6847f9e6bb84c083d68082ccf0a1be787fb9dd9c /plugins/syntax/string_syntax.ml | |
| parent | 0c60735279301d22ac3e03f862f86997cb85bce0 (diff) | |
Extraction: slightly better heuristic for Obj.magic simplifications
On an application (f args) where the head is magic, we first remove Obj.magic
on arguments before continuing with simplifications (that may push magic down
inside the arguments).
For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
before.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions