diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-25 13:31:45 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:52:43 +0200 |
commit | 3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 (patch) | |
tree | a4e4057e7057daca9edb1e78a3a9d8fcd584dc8f /test-suite/success/set.v | |
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 'test-suite/success/set.v')
0 files changed, 0 insertions, 0 deletions