package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/coq-core.vernac/Library/index.html
Module LibrarySource
This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that coincide with a file on disk (the ".vo" files). Libraries on the disk comes with checksums (obtained with the Digest module), which are checked at loading time to prevent inconsistencies between files written at various dates.
Type of libraries loaded in memory
Source
val intern_from_file :
CUnix.physical_path ->
(library_t, Exninfo.iexn) Result.t * Intern.Provenance.tSource
val require_library_syntax_from_dirpath :
intern:Intern.t ->
Names.DirPath.t Loc.located list ->
library_t listStart the compilation of a library
End the compilation of a library and save it to a ".vo" file, or a ".vos" file, depending on the todo_proofs argument.
output_native_objects: when producing vo objects, also compile the native-code version.
Source
val save_library_to :
'document todo_proofs ->
output_native_objects:bool ->
Names.DirPath.t ->
string ->
unitSave library to library_t format, that can be used later in require_library_syntax_from_dirpath
Interrogate the status of libraries
- Tell if a library is loaded
- Tell which libraries are loaded
Native compiler.
Opaque accessors