diff options
| author | Hugo Herbelin | 2016-06-12 16:00:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-12 16:03:39 +0200 |
| commit | 1f772656fa4bb6899ffea84ad5483e9690bbdc08 (patch) | |
| tree | 251fcc193bd523728bbb3e3509c0f4869618dfeb /kernel/type_errors.ml | |
| parent | 59e1618ccda6bbc9c627df93db7aaa3ea5930ccf (diff) | |
Reserve exception "ConversionFailed" in unification for failure of
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions