Module Coqloop

The Coq toplevel loop.

type input_buffer = {
mutable prompt : Stm.doc -> string;
mutable str : Stdlib.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

val top_buffer : input_buffer
val set_prompt : (unit -> string) -> unit
val coqloop_feed : Feedback.feedback -> unit

Toplevel feedback printer.

val drop_last_doc : Vernac.State.t option Stdlib.ref

Last document seen after `Drop`

val drop_args : Coqargs.t option Stdlib.ref
val loop : opts:Coqargs.t -> state:Vernac.State.t -> unit

Main entry point of Coq: read and execute vernac commands.