Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
val magic_number : int32
type 'a segment = private { name : string; pos : int64; len : int64; hash : Digest.t;}
type 'a id = private { id : string }(** Private to ensure the phantom tag is injective *)
type in_handletype out_handle
val make_id : string -> 'a id
val open_in : file:string -> in_handleval close_in : in_handle -> unitval marshal_in_segment : in_handle -> segment:'a id -> 'a * Digest.tval get_segment : in_handle -> segment:'a id -> 'a segmentval segments : in_handle -> Obj.t segment CString.Map.t
val open_out : file:string -> out_handleval close_out : out_handle -> unitval marshal_out_segment : out_handle -> segment:'a id -> 'a -> unitval marshal_out_binary : out_handle -> segment:'a id -> out_channel * (unit -> unit)(** [marshal_out_binary oh segment] is a low level, stateful, API returning [oc, stop]. Once called no other API can be used on the same [oh] and only [Stdlib.output_*] APIs should be used on [oc]. [stop ()] must be invoked in order to signal that all data was written to [oc] (which should not be used afterwards). Only after calling [stop] the other API can be used on [oh]. *)
val library_name : string -> string list(** For a given .vo (or .vos) filename return the library name stored in the "summary" segment (a dirpath, but we don't have access to Names.DirPath in this file) *)