diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 10 | ||||
| -rw-r--r-- | library/lib.ml | 23 | ||||
| -rw-r--r-- | library/lib.mli | 5 | ||||
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 1 |
6 files changed, 23 insertions, 26 deletions
diff --git a/library/global.ml b/library/global.ml index 315a147d2c..98d3e9cb1f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -102,15 +102,17 @@ 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 id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_private_constant id d = globalize (Safe_typing.add_private_constant (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) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) -let open_section ~poly = globalize0 (Safe_typing.open_section ~poly) +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 26ccb90271..f8b1f35f4d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,12 +46,14 @@ 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 + Id.t -> Safe_typing.global_declaration -> Constant.t +val add_private_constant : + Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -73,13 +75,15 @@ val add_include : (** Sections *) -val open_section : poly:bool -> unit +val open_section : unit -> unit (** [poly] is true when the section should be universe polymorphic *) 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 1c6f82e8a6..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 } @@ -425,9 +423,6 @@ let extract_worklist info = let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () -let is_polymorphic_univ u = - Section.is_polymorphic_univ u (sections ()) - let replacement_context () = Section.replacement_context (Global.env ()) (sections ()) @@ -464,11 +459,11 @@ let section_instance = let open GlobRef in function (*************) (* Sections. *) -let open_section ~poly id = - let () = Global.open_section ~poly in +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 5ce601f2d3..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 *) @@ -147,7 +148,7 @@ val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : poly:bool -> Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) @@ -183,8 +184,6 @@ val is_in_section : GlobRef.t -> bool val replacement_context : unit -> Opaqueproof.work_list -val is_polymorphic_univ : Univ.Level.t -> bool - (** {6 Discharge: decrease the section level if in the current section } *) (* XXX Why can't we use the kernel functions ? *) 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 |