diff options
| author | Pierre-Marie Pédrot | 2019-06-04 10:19:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-04 11:16:17 +0200 |
| commit | 0f54a91eac98baf076d8be8f52bccdb1de17ea46 (patch) | |
| tree | 5e6c7901f04577ba1fd4a4a05e09ff5df8cf4e76 /kernel | |
| parent | e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d (diff) | |
Slightly tweak the representation of dischargeable opaque proofs.
This will allow an easier removal of the discharge segment in a later
commit.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 4 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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 |