package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val require_library_from_dirpath : (Names.DirPath.t * string) list -> bool option -> unit
type seg_sum
type seg_lib
type seg_discharge = Opaqueproof.cooking_info list array
type seg_proofs = Constr.constr Future.computation array
val import_module : bool -> Libnames.qualid list -> unit
val start_library : CUnix.physical_path -> Names.DirPath.t
val save_library_to : ?todo:(((Future.UUID.t, 'document) Stateid.request * bool) list * 'counters) -> Names.DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo : string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * '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 library_is_opened : Names.DirPath.t -> bool
val loaded_libraries : unit -> Names.DirPath.t list
val opened_libraries : unit -> Names.DirPath.t list
val library_full_filename : Names.DirPath.t -> string
val overwrite_library_filenames : string -> unit
exception LibUnmappedDir
exception LibNotFound
type library_location =
  1. | LibLoaded
  2. | LibInPath
val locate_qualified_library : ?root:Names.DirPath.t -> ?warn:bool -> Libnames.qualid -> library_location * Names.DirPath.t * CUnix.physical_path
val native_name_from_filename : string -> string