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.toplevel/Coqloop/index.html
Module CoqloopSource
The Coq toplevel loop.
A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing.
Source
type input_buffer = {mutable prompt : Stm.doc -> string;mutable str : Bytes.t;(*buffer of already read characters
*)mutable len : int;(*number of chars in the buffer
*)mutable bols : int list;(*offsets in str of beginning of lines
*)mutable tokens : Pcoq.Parsable.t;(*stream of tokens
*)mutable start : int;
}stream count of the first char of the buffer
The input buffer of stdin.
Toplevel feedback printer.
State tracked while in the OCaml toplevel
Whether the "include" file was already run at least once
The main loop
Main entry point of Coq: read and execute vernac commands.