package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val require_library_from_dirpath : lib_resolver:(Names.DirPath.t -> CUnix.physical_path) -> (Names.DirPath.t * string) list -> bool option -> unit
type seg_sum
type seg_lib
type seg_univ = Univ.ContextSet.t * bool
type seg_proofs = Opaqueproof.opaque_proofterm array
type (!'document, !'counters) todo_proofs =
  1. | ProofsTodoNone
  2. | ProofsTodoSomeEmpty of Future.UUIDSet.t
  3. | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t, 'document) Stateid.request * bool) list * 'counters
val save_library_to : ('document, 'counters) todo_proofs -> output_native_objects:bool -> Names.DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo : CUnix.physical_path -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
val library_is_loaded : Names.DirPath.t -> bool
val loaded_libraries : unit -> Names.DirPath.t list
val library_full_filename : Names.DirPath.t -> string
val overwrite_library_filenames : string -> unit
val native_name_from_filename : string -> string
val indirect_accessor : Opaqueproof.indirect_accessor