diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 22 | ||||
| -rw-r--r-- | library/library.mli | 4 |
2 files changed, 8 insertions, 18 deletions
diff --git a/library/library.ml b/library/library.ml index 9f4eb531ed..3bc2e84054 100644 --- a/library/library.ml +++ b/library/library.ml @@ -276,8 +276,8 @@ let in_import_library : DirPath.t list * bool -> obj = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a Future.computation array delayed - | Fetched of 'a Future.computation array + | ToFetch of 'a option array delayed + | Fetched of 'a option array let opaque_tables = ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) @@ -315,7 +315,7 @@ let access_opaque_table dp i = let access_univ_table dp i = try let what = "universe contexts of opaque proofs" in - Some (access_table what univ_tables dp i) + access_table what univ_tables dp i with Not_found -> None let () = @@ -328,9 +328,9 @@ let () = type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array let mk_library sd md digests univs = { @@ -590,7 +590,7 @@ let save_library_to ?todo ~output_native_objects dir f otab = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in + let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab, dtab = match todo with | None -> None, None, None @@ -603,16 +603,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in - let except = - Future.UUIDSet.fold (fun uuid acc -> - try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc - with Not_found -> acc) - except Int.Set.empty in - let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in - Array.iteri (fun i x -> - if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" - Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) - opaque_table; let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); diff --git a/library/library.mli b/library/library.mli index f3186d847f..d2b0c4f202 100644 --- a/library/library.mli +++ b/library/library.mli @@ -34,9 +34,9 @@ val require_library_from_dirpath type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) |