Module Opaques.Summary

type t
val init : unit -> unit
val freeze : unit -> t
val unfreeze : t -> unit
val join : ?except:Future.UUIDSet.t -> unit -> unit

Force the certificate of every entry that is not already filled and whose UUID is not in except, filling the corresponding hole in the global environment. Entries keep the Future.computation that computed their certificate.

val inline : ?except:Future.UUIDSet.t -> unit -> unit

Same as join, and then replace each joined certificate by the proof term it certifies, the projection get_current_opaque already performs on read. The table denotes the same proofs but holds no Future.computation, so it survives marshalling: a certificate lives behind a CEphemeron.key, which loses its value when marshalled. Entries skipped through except keep theirs.

get_current_constraints and the map returned by dump only report certificates, so neither sees an inlined entry any more.