diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 6 | ||||
| -rw-r--r-- | library/lib.ml | 16 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 1 |
6 files changed, 15 insertions, 16 deletions
diff --git a/library/global.ml b/library/global.ml index c4685370d1..24cfc57f28 100644 --- a/library/global.ml +++ b/library/global.ml @@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) -let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) +let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) +let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) @@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) let open_section () = globalize0 Safe_typing.open_section let close_section fs = globalize0_with_summary fs Safe_typing.close_section +let sections_are_opened () = Safe_typing.sections_are_opened (safe_env()) let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index c45bf65d84..d689771f0a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit -val export_private_constants : in_section:bool -> +val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a + side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit (** Close the section and reset the global state to the one at the time when the section what opened. *) +val sections_are_opened : unit -> bool + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t diff --git a/library/lib.ml b/library/lib.ml index 0d9efe2d5d..80b50b26d0 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -107,7 +107,6 @@ let segment_of_objects prefix = let initial_prefix = Nametab.{ obj_dir = default_library; obj_mp = ModPath.initial; - obj_sec = DirPath.empty; } type lib_state = { @@ -132,10 +131,10 @@ let library_dp () = let cwd () = !lib_state.path_prefix.Nametab.obj_dir let current_mp () = !lib_state.path_prefix.Nametab.obj_mp -let current_sections () = !lib_state.path_prefix.Nametab.obj_sec +let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env()) -let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) -let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) +let sections_depth () = Section.depth (current_sections()) +let sections_are_opened = Global.sections_are_opened let cwd_except_section () = Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) @@ -169,7 +168,6 @@ let pop_path_prefix () = let op = !lib_state.path_prefix in lib_state := { !lib_state with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir; - obj_sec = pop_dirpath op.obj_sec; } } let find_entry_p p = @@ -282,7 +280,7 @@ let current_mod_id () = let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in - let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in + let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_dir dir @@ -330,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then + if Global.sections_are_opened () then (* XXX not sure if we need this check *) user_err Pp.(str "some sections are already opened"); - let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } @@ -465,7 +463,7 @@ let open_section id = let () = Global.open_section () in let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in - let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in if Nametab.exists_dir obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:false in diff --git a/library/lib.mli b/library/lib.mli index 59d77480e9..cef50a5f3b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool +[@@ocaml.deprecated "Use Global.sections_are_opened"] val sections_depth : unit -> int (** Are we inside an opened module type *) diff --git a/library/nametab.ml b/library/nametab.ml index aed7d08ac1..8626ee1c59 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,12 +18,10 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } let eq_op op1 op2 = DirPath.equal op1.obj_dir op2.obj_dir && - DirPath.equal op1.obj_sec op2.obj_sec && ModPath.equal op1.obj_mp op2.obj_mp (* to this type are mapped DirPath.t's in the nametab *) diff --git a/library/nametab.mli b/library/nametab.mli index 6ee22fc283..55458fe2c6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -74,7 +74,6 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } val eq_op : object_prefix -> object_prefix -> bool |