Module Vernac

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 -> interactive:bool -> state:State.t -> ?ldir:Names.DirPath.t -> 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.