diff options
| -rw-r--r-- | checker/values.ml | 2 | ||||
| -rw-r--r-- | library/declaremods.ml | 16 | ||||
| -rw-r--r-- | library/declaremods.mli | 11 | ||||
| -rw-r--r-- | library/lib.ml | 9 | ||||
| -rw-r--r-- | library/libobject.ml | 2 | ||||
| -rw-r--r-- | library/libobject.mli | 2 | ||||
| -rw-r--r-- | printing/printmod.ml | 2 | ||||
| -rw-r--r-- | vernac/library.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
9 files changed, 22 insertions, 30 deletions
diff --git a/checker/values.ml b/checker/values.ml index 708419e7cc..1590097731 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0, [| v_substobjs |]; [| v_aobjs |]; [| v_libobjs |]; - [| v_bool; v_mp |]; + [| v_mp |]; [| v_obj |] |]) diff --git a/library/declaremods.ml b/library/declaremods.ml index 301e5a3431..50cf7245bc 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -110,9 +110,9 @@ and subst_objects subst seg = | IncludeObject aobjs -> let aobjs' = subst_aobjs subst aobjs in if aobjs' == aobjs then node else (id, IncludeObject aobjs') - | ImportObject { export; mp } -> + | ExportObject { mp } -> let mp' = subst_mp subst mp in - if mp'==mp then node else (id, ImportObject { export; mp = mp' }) + if mp'==mp then node else (id, ExportObject { mp = mp' }) | KeepObject _ -> assert false in List.Smart.map subst_one seg @@ -249,7 +249,7 @@ let rec load_object i (name, obj) = let (sp,kn) = name in load_modtype i sp (mp_of_kn kn) sobjs | IncludeObject aobjs -> load_include i (name, aobjs) - | ImportObject _ -> () + | ExportObject _ -> () | KeepObject objs -> load_keep i (name, objs) and load_objects i prefix objs = @@ -289,7 +289,7 @@ and open_object i (name, obj) = | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs) | ModuleTypeObject sobjs -> open_modtype i (name, sobjs) | IncludeObject aobjs -> open_include i (name, aobjs) - | ImportObject { mp; _ } -> open_import i mp + | ExportObject { mp; _ } -> open_export i mp | KeepObject objs -> open_keep i (name, objs) and open_objects i prefix objs = @@ -312,7 +312,7 @@ and open_include i ((sp,kn), aobjs) = let o = expand_aobjs aobjs in open_objects i prefix o -and open_import i mp = +and open_export i mp = if Int.equal i 1 then really_import_module mp and open_keep i ((sp,kn),kobjs) = @@ -328,7 +328,7 @@ let rec cache_object (name, obj) = let (sp,kn) = name in load_modtype 0 sp (mp_of_kn kn) sobjs | IncludeObject aobjs -> cache_include (name, aobjs) - | ImportObject { mp } -> really_import_module mp + | ExportObject { mp } -> really_import_module mp | KeepObject objs -> cache_keep (name, objs) and cache_include ((sp,kn), aobjs) = @@ -975,9 +975,9 @@ let end_library ?except ~output_native_objects dir = let substitute, keep, _ = Lib.classify_segment lib_stack in cenv,(substitute,keep),ast -let import_module export mp = +let import_module ~export mp = really_import_module mp; - Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp })) + if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mp })) (** {6 Iterators} *) diff --git a/library/declaremods.mli b/library/declaremods.mli index ada53dbff0..c1d2de9783 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -103,18 +103,13 @@ val end_library : (** append a function to be executed at end_library *) val append_end_library_hook : (unit -> unit) -> unit -(** [really_import_module mp] opens the module [mp] (in a Caml sense). +(** [import_module export mp] imports the module [mp]. It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown - or when [mp] corresponds to a functor. *) - -val really_import_module : ModPath.t -> unit - -(** [import_module export mp] is a synchronous version of - [really_import_module]. If [export] is [true], the module is also + or when [mp] corresponds to a functor. If [export] is [true], the module is also opened every time the module containing it is. *) -val import_module : bool -> ModPath.t -> unit +val import_module : export:bool -> ModPath.t -> unit (** Include *) diff --git a/library/lib.ml b/library/lib.ml index 3f51826315..851f086961 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -73,11 +73,8 @@ let classify_segment seg = clean ((id,o)::substl, keepl, anticipl) stk | KeepObject _ -> clean (substl, (id,o)::keepl, anticipl) stk - | ImportObject { export } -> - if export then - clean ((id,o)::substl, keepl, anticipl) stk - else - clean acc stk + | ExportObject _ -> + clean ((id,o)::substl, keepl, anticipl) stk | AtomicObject obj -> begin match classify_object obj with | Dispose -> clean acc stk @@ -615,7 +612,7 @@ let discharge_item ((sp,_ as oname),e) = | Leaf lobj -> begin match lobj with | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _ - | ImportObject _ -> None + | ExportObject _ -> None | AtomicObject obj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj)) end diff --git a/library/libobject.ml b/library/libobject.ml index 27e7810e6c..3d4a33c74e 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -75,7 +75,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ImportObject of { export : bool; mp : ModPath.t } + | ExportObject of { mp : ModPath.t } | AtomicObject of obj and objects = (Names.Id.t * t) list diff --git a/library/libobject.mli b/library/libobject.mli index 3b37db4a6f..88d292ad03 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -112,7 +112,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ImportObject of { export : bool; mp : Names.ModPath.t } + | ExportObject of { mp : Names.ModPath.t } | AtomicObject of obj and objects = (Names.Id.t * t) list diff --git a/printing/printmod.ml b/printing/printmod.ml index 43992ec9d3..141469ff9c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -242,7 +242,7 @@ let nametab_register_body mp dir (l,body) = let nametab_register_module_body mp struc = (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.really_import_module mp + try Declaremods.import_module ~export:false mp with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) nametab_register_dir mp; 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 |