diff options
| -rw-r--r-- | checker/check.ml | 7 | ||||
| -rw-r--r-- | checker/values.ml | 2 | ||||
| -rw-r--r-- | kernel/opaqueproof.ml | 4 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 14 | ||||
| -rw-r--r-- | library/library.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 2 |
7 files changed, 17 insertions, 16 deletions
diff --git a/checker/check.ml b/checker/check.ml index 747d7c43a1..030b605e3f 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -51,7 +51,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t type seg_univ = Univ.ContextSet.t * bool -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr) option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array type library_t = { library_name : compilation_unit_name; @@ -98,9 +98,10 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - match t.(i) with + let (info, n, c) = t.(i) in + match c with | None -> None - | Some (info, n, c) -> Some (Cooking.cook_constr info n c) + | Some c -> Some (Cooking.cook_constr info n c) let access_discharge = Cooking.cook_constr diff --git a/checker/values.ml b/checker/values.ml index 6dbf281f49..4a4c8d803c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -399,6 +399,6 @@ let v_abstract = let v_cooking_info = Tuple ("cooking_info", [|v_work_list; v_abstract|]) -let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |]))) +let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index ee549dee4f..02d8ff0672 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -129,7 +129,7 @@ let get_direct_constraints = function module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n None in + let opaque_table = Array.make n ([], 0, None) in let disch_table = Array.make n [] in let f2t_map = ref FMap.empty in let iter n (univs, d, cu) = @@ -137,7 +137,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in if Future.is_val cu then let (c, _) = Future.force cu in - opaque_table.(n) <- Some (d, univs, c) + opaque_table.(n) <- (d, univs, Some c) else if Future.UUIDSet.mem uid except then (* Only monomorphic constraints can be delayed currently *) let () = assert (Int.equal univs 0) in diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 47439a787d..41f5ebb6b3 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -65,6 +65,6 @@ val discharge_direct_opaque : val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : ?except:Future.UUIDSet.t -> opaquetab -> - (cooking_info list * int * Constr.t) option array * + (cooking_info list * int * Constr.t option) array * cooking_info list array * int Future.UUIDMap.t diff --git a/library/library.ml b/library/library.ml index 0a57a85c35..8030b835be 100644 --- a/library/library.ml +++ b/library/library.ml @@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a option array delayed - | Fetched of 'a option array + | ToFetch of 'a array delayed + | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr) table_status) LibraryMap.t) + ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -306,10 +306,10 @@ let access_table what tables dp i = let access_opaque_table dp i = let what = "opaque proofs" in - let ans = access_table what opaque_tables dp i in - match ans with + let (info, n, c) = access_table what opaque_tables dp i in + match c with | None -> None - | Some (info, n, c) -> Some (Cooking.cook_constr info n c) + | Some c -> Some (Cooking.cook_constr info n c) let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; @@ -324,7 +324,7 @@ type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array let mk_library sd md digests univs = { diff --git a/library/library.mli b/library/library.mli index 0c5d6e33c1..284c66db5b 100644 --- a/library/library.mli +++ b/library/library.mli @@ -36,7 +36,7 @@ type seg_lib type seg_univ = (* all_cst, finished? *) Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) diff --git a/stm/stm.ml b/stm/stm.ml index 8efb606ddc..ad18245dec 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1747,7 +1747,7 @@ end = struct (* {{{ *) (* We only manipulate monomorphic terms here. *) let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr); + p.(bucket) <- d.(bucket), Univ.AUContext.size ctx, Some pr; Univ.ContextSet.union cst uc, false let check_task name l i = |