diff options
| author | Brian Campbell | 2018-06-26 12:19:37 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-26 12:23:59 +0100 |
| commit | d2ff50391bff188c45dfbc410f4fb16b4fd3bbce (patch) | |
| tree | 812d33a80871cdb4d4291d203c867a917ad6f60a /src/bytecode_util.ml | |
| parent | 2e529d7f5261749d0a1463283020f56265ad2e9a (diff) | |
In guarded pattern rewriting, irrefutable patterns subsume wildcards
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
Diffstat (limited to 'src/bytecode_util.ml')
0 files changed, 0 insertions, 0 deletions