diff options
| author | Pierre-Marie Pédrot | 2018-10-25 13:31:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-29 17:47:15 +0100 |
| commit | d5e762723bca7cb9297183e4332e0a9c7c0932f0 (patch) | |
| tree | 9eb7b8bf161c210a9c5b676e97fd09ff742daf0d /doc/plugin_tutorial/tuto1/src/simple_check.mli | |
| parent | 9ead21a38feae29fdde11344de326de86bfe8ad9 (diff) | |
Do not compare the type arguments in pattern-match branches.
We know that the two are living in a common type, so that it is useless
to perform the comparison check. Note that we only use this fast-path when
the branches are only made of lambda-abstractions, but this covers
all actual cases.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.mli')
0 files changed, 0 insertions, 0 deletions