diff options
| author | Pierre Letouzey | 2017-02-04 19:29:15 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2017-02-07 22:56:56 +0100 |
| commit | af4962a9211a707943e7b0627439a731c3e7d23f (patch) | |
| tree | 3e9271239bd0ba876cd8d8060c951930fa45907a /kernel/type_errors.ml | |
| parent | c04f336b2efb43401dee3a5bb9dceaeac815ef00 (diff) | |
Extraction : get_duplicates (via option) instead of check_duplicates (via Not_found)
This clarifies the execution flow
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions