diff options
| author | Hugo Herbelin | 2016-04-25 13:31:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:52:43 +0200 |
| commit | 3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 (patch) | |
| tree | a4e4057e7057daca9edb1e78a3a9d8fcd584dc8f /kernel | |
| parent | 2ee92b2e851c91776ed26b2461304867b0b8c98c (diff) | |
Optimization in building a return clause by pattern-matching: do not
build a default case if the pattern is irrefutable. It did not matter
in practice because we did not check for unused clauses in this case.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
