aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/set.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-25 13:31:45 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 21:52:43 +0200
commit3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 (patch)
treea4e4057e7057daca9edb1e78a3a9d8fcd584dc8f /test-suite/success/set.v
parent2ee92b2e851c91776ed26b2461304867b0b8c98c (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 'test-suite/success/set.v')
0 files changed, 0 insertions, 0 deletions