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.