diff options
| author | Hugo Herbelin | 2015-04-21 16:36:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-21 16:36:31 +0200 |
| commit | a45bd5981092cceefc4d4d30f9be327bb69c22d8 (patch) | |
| tree | c21b83ba996432b1e2fefa8b916eac4fec038b94 /lib/errors.mli | |
| parent | 9fa7f38b74ec26f880d9ec983a5a1c8699e0a612 (diff) | |
Fixing #4198 (looking for subterms also in the return clause of match).
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
Diffstat (limited to 'lib/errors.mli')
0 files changed, 0 insertions, 0 deletions