Module `Vernac`

type time_output

val make_time_output : Coqargs.time_config -> time_output

module State : sig ... end: Parsing of vernacular.

val process_expr : state:State.t -> Vernacexpr.vernac_control -> State.t: process_expr sid cmd Executes vernac command cmd. Callers are expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state.

val load_vernac : echo:bool -> check:bool -> state:State.t -> ?⁠source:Loc.source -> string -> State.t: load_vernac echo sid file Loads file on top of sid, will echo the commands if echo is set. Callers are expected to handle and print errors in form of exceptions.