diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 7 | ||||
| -rw-r--r-- | library/lib.ml | 3 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | library/libnames.ml | 3 | ||||
| -rw-r--r-- | library/libnames.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 19 | ||||
| -rw-r--r-- | library/library.mli | 2 |
8 files changed, 21 insertions, 20 deletions
diff --git a/library/global.ml b/library/global.ml index 06e06a8cf2..58e2380440 100644 --- a/library/global.ml +++ b/library/global.ml @@ -94,7 +94,8 @@ 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 ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d) +let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) +let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (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) diff --git a/library/global.mli b/library/global.mli index a60de48897..984d8c666c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,8 @@ val export_private_constants : in_section:bool -> unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : - in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t + ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants +val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -84,7 +85,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Constr.named_declaration -val lookup_constant : Constant.t -> Declarations.constant_body +val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> @@ -105,7 +106,7 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) diff --git a/library/lib.ml b/library/lib.ml index a046360822..4be288ed20 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -211,9 +211,6 @@ let split_lib_at_opening sp = let add_entry sp node = lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } -let pull_to_head oname = - lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } - let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index 30569197bc..5da76961a6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -57,7 +57,6 @@ val segment_of_objects : val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) diff --git a/library/libnames.ml b/library/libnames.ml index 87c4de42e8..41b38e0378 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,6 +162,9 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath +let idset_mem_qualid qid s = + qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s + (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index bbb4d2a058..7d77d95991 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t +val idset_mem_qualid : qualid -> Id.Set.t -> bool +(** false when the qualid is not an ident *) + (** {6 ... } *) (** some preset paths *) diff --git a/library/library.ml b/library/library.ml index 04e38296d9..500e77f89b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -612,8 +612,6 @@ let import_module export modl = (*s Initializing the compilation of a library. *) let load_library_todo f = - let longf = Loadpath.locate_file (f^".v") in - let f = longf^"io" in let ch = raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in @@ -626,7 +624,7 @@ let load_library_todo f = if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -727,14 +725,13 @@ let save_library_to ?todo ~output_native_objects dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^"o" in - let ch = raw_extern_library f' in - System.marshal_out_segment f' ch (sum : seg_sum); - System.marshal_out_segment f' ch (lib : seg_lib); - System.marshal_out_segment f' ch (Some univs : seg_univ option); - System.marshal_out_segment f' ch (None : seg_discharge option); - System.marshal_out_segment f' ch (None : 'tasks option); - System.marshal_out_segment f' ch (proofs : seg_proofs); + let ch = raw_extern_library f in + System.marshal_out_segment f ch (sum : seg_sum); + System.marshal_out_segment f ch (lib : seg_lib); + System.marshal_out_segment f ch (Some univs : seg_univ option); + System.marshal_out_segment f ch (None : seg_discharge option); + System.marshal_out_segment f ch (None : 'tasks option); + System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch module StringOrd = struct type t = string let compare = String.compare end diff --git a/library/library.mli b/library/library.mli index a976be0184..390299bf56 100644 --- a/library/library.mli +++ b/library/library.mli @@ -46,7 +46,7 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) |