diff options
| author | Maxime Dénès | 2019-06-11 10:49:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-28 13:28:03 +0200 |
| commit | 19ea68ecafcee5199dde1b044fd4be9edc211673 (patch) | |
| tree | f6a6fec1e8825371cbdab78931d0dd5c831dd15b /library/library.ml | |
| parent | a4f6189978b15df8ce4cc8c8fcb8acb6f069ee8e (diff) | |
Reify libobject containers
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index 0d4148d7e4..b72dd9dd67 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,7 +488,7 @@ let require_library_from_dirpath ~lib_resolver modrefl export = let safe_locate_module qid = try Nametab.locate_module qid with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_library" + user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module" (pr_qualid qid ++ str " is not a module") let import_module export modl = @@ -513,7 +513,7 @@ let import_module export modl = flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_library" + user_err ?loc:qid.CAst.loc ~hdr:"import_module" (pr_qualid qid ++ str " is not a module")) | [] -> flush acc in aux [] modl |