diff options
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 |