package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.vernac/Library/index.html
Module Library
Source
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.t
Source
val require_library_syntax_from_dirpath :
intern:Intern.t ->
Names.DirPath.t Loc.located list ->
library_t list
Start 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 ->
unit
Save 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page