diff options
| author | Hugo Herbelin | 2016-06-12 16:06:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-12 16:06:43 +0200 |
| commit | 19aa7231ec96dbbfdda7788679cf7ddf00bda7a5 (patch) | |
| tree | 12d614854144384191fb04637498297810020cd9 /kernel/type_errors.ml | |
| parent | 827663982e9cdf502f21727677515cf2318aa41d (diff) | |
Minor simplification in evarconv.
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions