diff options
| author | Pierre-Marie Pédrot | 2019-06-04 13:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:02 +0200 |
| commit | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (patch) | |
| tree | 8016562d06949b981a3e58e71103b02aea7f1c44 /library/library.ml | |
| parent | 7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff) | |
Allow to delay polymorphic opaque constants.
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/library/library.ml b/library/library.ml index 1ac75d2fdc..a55fe33617 100644 --- a/library/library.ml +++ b/library/library.ml @@ -280,7 +280,7 @@ type 'a table_status = | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t) + ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -306,10 +306,7 @@ let access_table what tables dp i = let access_opaque_table dp i = let what = "opaque proofs" in - let (info, n, c) = access_table what opaque_tables dp i in - match c with - | None -> None - | Some c -> Some (Cooking.cook_constr info n c) + access_table what opaque_tables dp i let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; @@ -323,7 +320,7 @@ type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) Univ.ContextSet.t * bool -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array +type seg_proofs = Opaqueproof.opaque_proofterm array let mk_library sd md digests univs = { |