diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 15:44:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 20:22:35 +0200 |
| commit | b7b78d8ca8d6fc6fdb0f744be02c386bc00da8bf (patch) | |
| tree | 9f9c03e501a207c70c7b518f431c744062140ddc /kernel/type_errors.ml | |
| parent | 8b2505b5526395d2ad3c5126624a070e0f55a8af (diff) | |
[loadpath] Further cleanup after merge with MlTop.
We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.
In particular, we remove exceptions in favor a `locate_result` monad.
More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions