diff options
| author | Maxime Dénès | 2019-07-08 15:00:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-16 09:56:58 +0200 |
| commit | 4614010ceddb9ed5100fa4e43d2807b172143a19 (patch) | |
| tree | 79fbcf2cb11e04765b5736399c85cb06ac5298c4 /vernac | |
| parent | 2957e86c93556b0baf86b662d34fce1a2096edc2 (diff) | |
Specialize `ImportObject` to `Export`
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index ed29ebecd3..437ec7961e 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -340,7 +340,7 @@ let load_require _ (_,(needed,modl,_)) = List.iter register_library needed let open_require i (_,(_,modl,export)) = - Option.iter (fun exp -> List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modl) + Option.iter (fun export -> List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modl) export (* [needed] is the ordered list of libraries not already loaded *) @@ -380,8 +380,8 @@ let require_library_from_dirpath ~lib_resolver modrefl export = begin warn_require_in_module (); add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - List.iter (fun m -> Declaremods.import_module exp (MPfile m)) modrefl) + Option.iter (fun export -> + List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl) export end else diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index adfe469811..43b58d6d4b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -856,7 +856,7 @@ let vernac_constraint ~poly l = let vernac_import export refl = let import_mod qid = - try Declaremods.import_module export @@ Nametab.locate_module qid + try Declaremods.import_module ~export @@ Nametab.locate_module qid with Not_found -> CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid) in |